Exofunctor.idr

module Data.Exofunctor

import Data.Morphisms

%access public export
%default total

-- replace Control.Category with this
interface Category (cat : k -> k -> Type) where
  id  : cat a a
  (.) : cat b c -> cat a b -> cat a c

implementation Category Morphism where
  id = Mor id
  -- disambiguation needed below, because unification can now get further
  -- here with Category.(.) and it's only interface resolution that fails!
  (Mor f) . (Mor g) = with Basics (Mor (f . g))

data NaturalTransformation : (cat : k -> k -> Type) -> (f : j -> k) -> (g : j -> k) -> Type where
  Natural : ({x : j} -> cat (f x) (g x)) -> NaturalTransformation cat f g

implementation Category cat => Category (NaturalTransformation cat) where
  id                        = Natural id
  (Natural c) . (Natural d) = Natural (c . d)

||| A category with objects of `obj` has arrows of `Cat obj`.
Cat : (obj : Type) -> obj -> obj -> Type
Cat Type     = Morphism -- The category `Idr`
-- Cat (a -> b) = NaturalTransformation (Cat b)

-- TODO: Any way to make `j` and `k` implicit?
interface (Category (Cat j), Category (Cat k)) => Exofunctor j k (f : j -> k) | f where
  emap : Cat j a b -> Cat k (f a) (f b)
  
||| Lift all the “usual” `Functor`s into `Exofunctor`. Ideally, `Exofunctor`
||| would be a drop-in replacement for `Functor`, but `Morphism` gets in the
||| way.
implementation Functor f => Exofunctor Type Type f where
  emap (Mor f) = Mor (map f)
  
-- NB: These are implied by the previous implementation
--
-- implementation Exofunctor Type Type Maybe where
--   emap (Mor f) = Mor (\a => case a of
--                          Nothing => Nothing
--                          Just a  => Just (f a))

-- implementation Exofunctor Type Type (Either e) where
--   emap (Mor f) = Mor (\a => case a of
--                          Left e  => Left e
--                          Right a => Right (f a))