0 | module Data.Morphisms
  1 |
  2 | import Data.Contravariant
  3 |
  4 | %default total
  5 |
  6 | public export
  7 | record Morphism a b where
  8 |   constructor Mor
  9 |   applyMor : a -> b
 10 |
 11 | export infixr 1 ~>
 12 |
 13 | public export
 14 | (~>) : Type -> Type -> Type
 15 | (~>) = Morphism
 16 |
 17 | public export
 18 | record Endomorphism a where
 19 |   constructor Endo
 20 |   applyEndo : a -> a
 21 |
 22 | public export
 23 | record Kleislimorphism (f : Type -> Type) a b where
 24 |   constructor Kleisli
 25 |   applyKleisli : a -> f b
 26 |
 27 | public export
 28 | record Op b a where
 29 |   constructor MkOp
 30 |   applyOp : a -> b
 31 |
 32 | export
 33 | Functor (Morphism r) where
 34 |   map f (Mor a) = Mor $ f . a
 35 |
 36 | export
 37 | Applicative (Morphism r) where
 38 |   pure a = Mor $ const a
 39 |   (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r
 40 |
 41 | export
 42 | Monad (Morphism r) where
 43 |   (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r
 44 |
 45 | export
 46 | Semigroup a => Semigroup (Morphism r a) where
 47 |   f <+> g = Mor $ \r => (applyMor f) r <+> (applyMor g) r
 48 |
 49 | export
 50 | Monoid a => Monoid (Morphism r a) where
 51 |   neutral = Mor $ \_ => neutral
 52 |
 53 | export
 54 | Semigroup (Endomorphism a) where
 55 |   (Endo f) <+> (Endo g) = Endo $ g . f
 56 |
 57 | export
 58 | Monoid (Endomorphism a) where
 59 |   neutral = Endo id
 60 |
 61 | export
 62 | Functor f => Functor (Kleislimorphism f a) where
 63 |   map f (Kleisli g) = Kleisli (map f . g)
 64 |
 65 | export
 66 | Applicative f => Applicative (Kleislimorphism f a) where
 67 |   pure a = Kleisli $ const $ pure a
 68 |   (Kleisli f) <*> (Kleisli a) = Kleisli $ \r => f r <*> a r
 69 |
 70 | export
 71 | Monad f => Monad (Kleislimorphism f a) where
 72 |   (Kleisli f) >>= g = Kleisli $ \r => do
 73 |     k1 <- f r
 74 |     applyKleisli (g k1) r
 75 |
 76 | public export
 77 | Contravariant (Op b) where
 78 |   contramap f (MkOp g) = MkOp (g . f)
 79 |   v >$ (MkOp f) = MkOp $ \_ => f v
 80 |
 81 | -- Applicative is a bit too strong, but there is no suitable superclass
 82 | export
 83 | (Semigroup a, Applicative f) => Semigroup (Kleislimorphism f r a) where
 84 |   f <+> g = Kleisli $ \r => (<+>) <$> (applyKleisli f) r <*> (applyKleisli g) r
 85 |
 86 | export
 87 | (Monoid a, Applicative f) => Monoid (Kleislimorphism f r a) where
 88 |   neutral = Kleisli $ \_ => pure neutral
 89 |
 90 | export
 91 | Cast (Endomorphism a) (Morphism a a) where
 92 |   cast (Endo f) = Mor f
 93 |
 94 | export
 95 | Cast (Morphism a a) (Endomorphism a) where
 96 |   cast (Mor f) = Endo f
 97 |
 98 | export
 99 | Cast (Morphism a (f b)) (Kleislimorphism f a b) where
100 |   cast (Mor f) = Kleisli f
101 |
102 | export
103 | Cast (Kleislimorphism f a b) (Morphism a (f b)) where
104 |   cast (Kleisli f) = Mor f
105 |
106 | export
107 | Cast (Endomorphism a) (Op a a) where
108 |   cast (Endo f) = MkOp f
109 |
110 | export
111 | Cast (Op a a) (Endomorphism a) where
112 |   cast (MkOp f) = Endo f
113 |
114 | export
115 | Cast (Op (f b) a) (Kleislimorphism f a b) where
116 |   cast (MkOp f) = Kleisli f
117 |
118 | export
119 | Cast (Kleislimorphism f a b) (Op (f b) a) where
120 |   cast (Kleisli f) = MkOp f
121 |
122 | export
123 | Cast (Morphism a b) (Op b a) where
124 |   cast (Mor f) = MkOp f
125 |
126 | export
127 | Cast (Op b a) (Morphism a b) where
128 |   cast (MkOp f) = Mor f
129 |