0 | module Control.Monad.Continuation
 1 |
 2 | import public Control.Monad.Trans
 3 | import public Control.Monad.Identity
 4 |
 5 | public export
 6 | record ContT {0 ty : Type} (r : ty) (m : ty -> Type) (a : Type) where
 7 |   constructor MkContT
 8 |   contT : (a -> m r) -> m r
 9 |
10 | export %inline
11 | runCont : Applicative m => ContT () m () -> m ()
12 | runCont = ($ pure) . contT
13 |
14 | export %inline
15 | MonadTrans (ContT r) where
16 |   lift m = MkContT (m >>=)
17 |
18 | export %inline
19 | Functor (ContT r m) where
20 |   map f c = MkContT (c.contT . (. f))
21 |
22 | export %inline
23 | Applicative (ContT r m) where
24 |   pure x = MkContT ($ x)
25 |   (<*>) (MkContT f) (MkContT x) =
26 |       MkContT $ \cb => f (x . (cb .))
27 |
28 | export %inline
29 | Monad (ContT r m) where
30 |   join n = MkContT $ \cb => n.contT (($ cb) . contT)
31 |
32 | export %inline
33 | HasIO m => HasIO (ContT r m) where
34 |   liftIO mio = MkContT (liftIO mio >>=)
35 |
36 | public export
37 | Cont : (r, a : Type) -> Type
38 | Cont r = ContT r Identity
39 |
40 |