Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.