@@ -1,45 +1,61 @@
11module Data.Morphisms
22
3+%default total
34%access public export
45
5−data Morphism : Type -> Type -> Type where
6− Mor : (a -> b) -> Morphism a b
7−
8−data Endomorphism : Type -> Type where
9− Endo : (a -> a) -> Endomorphism a
10−
11−data Kleislimorphism : (Type -> Type) -> Type -> Type -> Type where
12− Kleisli : Monad m => (a -> m b) -> Kleislimorphism m a b
13−
14−applyKleisli : Monad m => (Kleislimorphism m a b) -> a -> m b
15−applyKleisli (Kleisli f) a = f a
6+record Morphism a b where
7+ constructor Mor
8+ applyMor : a -> b
9+infixr 1 ~>
10+(~>) : Type -> Type -> Type
11+(~>) = Morphism
1612
17−applyMor : Morphism a b -> a -> b
18−applyMor (Mor f) a = f a
13+record Endomorphism a where
14+ constructor Endo
15+ applyEndo : a -> a
1916
20−applyEndo : Endomorphism a -> a -> a
21−applyEndo (Endo f) a = f a
17+record Kleislimorphism (f : Type -> Type) a b where
18+ constructor Kleisli
19+ applyKleisli : a -> f b
2220
23−implementation Functor (Morphism r) where
24− map f (Mor a) = Mor (f . a)
21+Functor (Morphism r) where
22+ map f (Mor a) = Mor $ f . a
2523
26−implementation Applicative (Morphism r) where
27− pure a = Mor $ const a
24+Applicative (Morphism r) where
25+ pure a = Mor $ const a
2826 (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r
2927
30−implementation Monad (Morphism r) where
28+Monad (Morphism r) where
3129 (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r
3230
33−implementation Semigroup (Endomorphism a) where
31+Semigroup a => Semigroup (Morphism r a) where
32+ f <+> g = [| f <+> g |]
33+
34+Monoid a => Monoid (Morphism r a) where
35+ neutral = [| neutral |]
36+
37+Semigroup (Endomorphism a) where
3438 (Endo f) <+> (Endo g) = Endo $ g . f
3539
36−implementation Monoid (Endomorphism a) where
40+Monoid (Endomorphism a) where
3741 neutral = Endo id
3842
39−infixr 1 ~>
43+Functor f => Functor (Kleislimorphism f a) where
44+ map f (Kleisli g) = Kleisli (map f . g)
4045
41−(~>) : Type -> Type -> Type
42−a ~> b = Morphism a b
46+Applicative f => Applicative (Kleislimorphism f a) where
47+ pure a = Kleisli $ const $ pure a
48+ (Kleisli f) <*> (Kleisli a) = Kleisli $ \r => f r <*> a r
49+
50+Monad f => Monad (Kleislimorphism f a) where
51+ (Kleisli f) >>= g = Kleisli $ \r => applyKleisli (g !(f r)) r
52+
53+-- Applicative is a bit too strong, but there is no suitable superclass
54+(Semigroup a, Applicative f) => Semigroup (Kleislimorphism f r a) where
55+ f <+> g = [| f <+> g |]
56+
57+(Monoid a, Applicative f) => Monoid (Kleislimorphism f r a) where
58+ neutral = [| neutral |]
4359
4460Cast (Endomorphism a) (Morphism a a) where
4561 cast (Endo f) = Mor f
@@ -47,8 +63,8 @@ Cast (Endomorphism a) (Morphism a a) where
4763Cast (Morphism a a) (Endomorphism a) where
4864 cast (Mor f) = Endo f
4965
50−Monad m => Cast (Morphism a (m b)) (Kleislimorphism m a b) where
66+Cast (Morphism a (f b)) (Kleislimorphism f a b) where
5167 cast (Mor f) = Kleisli f
5268
53−Cast (Kleislimorphism m a b) (Morphism a (m b)) where
69+Cast (Kleislimorphism f a b) (Morphism a (f b)) where
5470 cast (Kleisli f) = Mor f