
  0 | module Control.Monad.Free.Church
  1 | 
  2 | import Control.Monad.Trans
  3 | 
  4 | import Control.Monad.Free
  5 | 
  6 | record F (f : Type -> Type) (a : Type) where
  7 |   constructor MkF
  8 |   runF : forall z. (a -> z) -> (f z -> z) -> z
  9 | 
 10 | Functor (F f) where
 11 |   map f (MkF g) = MkF (\kp => g (kp . f))
 12 | 
 13 | Applicative (F f) where
 14 |   pure x = MkF (\kp, _ => kp x)
 15 |   MkF f <*> MkF g = MkF (\kp, kf => f (\a => g (kp . a) kf) kf)
 16 | 
 17 | Monad (F f) where
 18 |   MkF m >>= f = MkF (\kp, kf => m (\a => runF (f a) kp kf) kf)
 19 | 
 20 | MonadTrans F where
 21 |   lift f = MkF (\kp, kf => kf (liftM kp f))
 22 |     where liftM : (a -> b) -> m a -> m b
 23 |           liftM f m = pure $ f !m
 24 | 
 25 | {f : _} -> MonadFree f (F f) where
 26 |   wrap f = MkF (\kp, kf => kf (map (\(MkF m) => m kp kf) f))
 27 |