0 | module Control.Kleisli
 1 |
 2 | import Control.Category
 3 | import Data.Functor.Indexed
 4 | import Data.Filterable.Indexed
 5 |
 6 |
 7 | record Kleisli (m : Type -> Type) (a : Type) (b : Type) where
 8 |   constructor MkKleisli
 9 |   runKleisli : a -> m b
10 |
11 | Functor m => Functor (Kleisli m a) where
12 |   map f (MkKleisli p) = MkKleisli (map f . p)
13 |
14 | Functor m => IndFunctor a (Kleisli m a) where
15 |   imap f (MkKleisli p) = MkKleisli (\x => map (f x) (p x))
16 |
17 | Applicative m => Applicative (Kleisli m a) where
18 |   pure = MkKleisli . const . pure
19 |   MkKleisli p <*> MkKleisli q = MkKleisli (\x => p x <*> q x)
20 |
21 | Monad m => Monad (Kleisli m a) where
22 |   MkKleisli p >>= r = MkKleisli (\x => p x >>= (\a => runKleisli (r a) x))
23 |
24 | -- Haven't got this working yet
25 | {-
26 | Monad m => Category (Kleisli m) where
27 |   identity a = MkKleisli pure
28 |   cmp (MkKleisli g) (MkKleisli f) = MkKleisli (g <=< f)
29 | -}
30 |
31 | -- This belongs in with Alternative
32 | liftMaybe : Alternative m => Maybe a -> m a
33 | liftMaybe = maybe empty pure
34 |
35 | -- Why must the type be called a'? It's a little mysterious
36 | (Monad m, Alternative m) => Filterable (Kleisli m a') where
37 |   mapMaybe f (MkKleisli p) = MkKleisli (liftMaybe . f <=< p)
38 |   flush (MkKleisli p) = MkKleisli (const empty)
39 |
40 | (Monad m, Alternative m) => IndFilterable a (Kleisli m a) where
41 |   imapMaybe f (MkKleisli p) = MkKleisli (\x => liftMaybe . f x =<< p x)
42 |