
  0 | module Control.Monad.Trans.Free
  1 | 
  2 | import Control.Monad.Trans
  3 | 
  4 | import Control.Monad.Free
  5 | 
  6 | data FreeF : (f : Type -> Type) -> (a : Type) -> (b : Type) -> Type where
  7 |   Pure : a -> FreeF f a b
  8 |   Free : f b -> FreeF f a b
  9 | 
 10 | Functor f => Functor (FreeF f a) where
 11 |   map _ (Pure a)  = Pure a
 12 |   map g (Free as) = Free $ map g as
 13 | 
 14 | transFreeF : (forall x. f x -> g x) -> FreeF f a b -> FreeF g a b
 15 | transFreeF _   (Pure a)  = Pure a
 16 | transFreeF phi (Free as) = Free $ phi as
 17 | 
 18 | record FreeT f m a where
 19 |   constructor MkFreeT
 20 |   runFreeT : m (FreeF f a (FreeT f m a))
 21 | 
 22 | 
 23 | export
 24 | iterT : {f : _} -> (Functor f, Monad m) => (f (m a) -> m a) -> FreeT f m a -> m a
 25 | iterT f (MkFreeT m) = do
 26 |   val <- m
 27 |   case map (iterT f) val of
 28 |     Pure a  => pure a
 29 |     Free as => f as
 30 |