
  0 | module Control.Monad.Trans.Free.Church
  1 | 
  2 | import Control.Monad.Trans
  3 | 
  4 | import Control.Monad.Free
  5 | import Control.Monad.Free.Church
  6 | 
  7 | ||| Church-encoded free monad transformer. Translated from:
  8 | ||| https://hackage.haskell.org/package/free-5.1.8/docs/src/Control.Monad.Trans.Free.Church.html
  9 | public export
 10 | record FT (f : Type -> Type) (m : Type -> Type) (a : Type) where
 11 |   constructor MkFT
 12 |   runFT : forall r. (a -> m r) -> (forall x. (x -> m r) -> f x -> m r) -> m r
 13 | 
 14 | export
 15 | Functor (FT f m) where
 16 |   map f (MkFT k) = MkFT $ \kp, kf => k (kp . f) kf
 17 | 
 18 | export
 19 | Applicative (FT f m) where
 20 |   pure a =  MkFT (\k, _ => k a)
 21 |   (MkFT fk) <*> (MkFT ak) = MkFT $ \b, fr => fk (\e => ak (\d => b (e d)) fr) fr
 22 | 
 23 | export
 24 | Monad (FT f m) where
 25 |   (MkFT fk) >>= f = MkFT $ \b, fr => fk (\d => runFT (f d) b fr) fr
 26 | 
 27 | export
 28 | MonadTrans (FT f) where
 29 |   lift m = MkFT (\a, _ => m >>= a)
 30 | 
 31 | export
 32 | MonadFree f (FT f m) where
 33 |   wrap f = MkFT (\kp, kf => kf (\ft => runFT ft kp kf) f)
 34 | 
 35 | export
 36 | hoistFT : (Monad m, Monad n) => (forall x. m x -> n x) -> FT f m a -> FT f n a
 37 | hoistFT phi (MkFT m) = MkFT (\kp, kf => join . phi $ m (pure . kp) (\xg => pure . kf (join . phi . xg)))
 38 | 
 39 | export
 40 | iterT : (Functor f, Monad m) => (f (m a) -> m a) -> FT f m a -> m a
 41 | iterT f (MkFT m) = m pure (\xg => f . map xg)
 42 | 
 43 | export
 44 | iterTM : (Functor f, Monad m, MonadTrans t, Monad (t m)) => (f (t m a) -> t m a) -> FT f m a -> t m a
 45 | iterTM f (MkFT m) = join . lift $ m (pure . pure) (\xg => pure . f . map (join . lift . xg))
 46 |