@@ -1,45 +1,61 @@
1module Data.Morphisms
1module Data.Morphisms
3%access public export
4%access public export
5−data Morphism : Type -> Type -> Type where
6+record Morphism a b where
6− Mor : (a -> b) -> Morphism a b
7+ constructor Mor
8−data Endomorphism : Type -> Type where
9+infixr 1 ~>
9− Endo : (a -> a) -> Endomorphism a
11−data Kleislimorphism : (Type -> Type) -> Type -> Type -> Type where
10+(~>) : Type -> Type -> Type
12− Kleisli : Monad m => (a -> m b) -> Kleislimorphism m a b
11+(~>) = Morphism
14−applyKleisli : Monad m => (Kleislimorphism m a b) -> a -> m b
15−applyKleisli (Kleisli f) a = f a
17−applyMor : Morphism a b -> a -> b
13+record Endomorphism a where
18−applyMor (Mor f) a = f a
14+ constructor Endo
20−applyEndo : Endomorphism a -> a -> a
17+record Kleislimorphism (f : Type -> Type) a b where
21−applyEndo (Endo f) a = f a
18+ constructor Kleisli
19+ applyKleisli : a -> f b
23−implementation Functor (Morphism r) where
21+Functor (Morphism r) where
24− map f (Mor a) = Mor (f . a)
22+ map f (Mor a) = Mor $ f . a
26−implementation Applicative (Morphism r) where
24+Applicative (Morphism r) where
27− pure a = Mor $ const a
25+ pure a = Mor $ const a
28 (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r
26 (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r
30−implementation Monad (Morphism r) where
28+Monad (Morphism r) where
31 (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r
29 (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r
31+Semigroup a => Semigroup (Morphism r a) where
32+ f <+> g = [| f <+> g |]
34+Monoid a => Monoid (Morphism r a) where
35+ neutral = [| neutral |]
33−implementation Semigroup (Endomorphism a) where
37+Semigroup (Endomorphism a) where
34 (Endo f) <+> (Endo g) = Endo $ g . f
38 (Endo f) <+> (Endo g) = Endo $ g . f
36−implementation Monoid (Endomorphism a) where
40+Monoid (Endomorphism a) where
37 neutral = Endo id
41 neutral = Endo id
39−infixr 1 ~>
43+Functor f => Functor (Kleislimorphism f a) where
44+ map f (Kleisli g) = Kleisli (map f . g)
41−(~>) : Type -> Type -> Type
46+Applicative f => Applicative (Kleislimorphism f a) where
42−a ~> b = Morphism a b
47+ pure a = Kleisli $ const $ pure a
48+ (Kleisli f) <*> (Kleisli a) = Kleisli $ \r => f r <*> a r
50+Monad f => Monad (Kleislimorphism f a) where
51+ (Kleisli f) >>= g = Kleisli $ \r => applyKleisli (g !(f r)) r
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 |]
57+(Monoid a, Applicative f) => Monoid (Kleislimorphism f r a) where
58+ neutral = [| neutral |]
44Cast (Endomorphism a) (Morphism a a) where
60Cast (Endomorphism a) (Morphism a a) where
45 cast (Endo f) = Mor f
61 cast (Endo f) = Mor f
@@ -47,8 +63,8 @@ Cast (Endomorphism a) (Morphism a a) where
47Cast (Morphism a a) (Endomorphism a) where
63Cast (Morphism a a) (Endomorphism a) where
48 cast (Mor f) = Endo f
64 cast (Mor f) = Endo f
50−Monad m => Cast (Morphism a (m b)) (Kleislimorphism m a b) where
66+Cast (Morphism a (f b)) (Kleislimorphism f a b) where
51 cast (Mor f) = Kleisli f
67 cast (Mor f) = Kleisli f
53−Cast (Kleislimorphism m a b) (Morphism a (m b)) where
69+Cast (Kleislimorphism f a b) (Morphism a (f b)) where
54 cast (Kleisli f) = Mor f
70 cast (Kleisli f) = Mor f