
  0 | module Control.Monad.Free
  1 | 
  2 | import Control.EffectAlgebra
  3 | 
  4 | ||| Higher-order free monad.
  5 | ||| Acts as a syntax generator of effectful programs.
  6 | public export
  7 | data Free : (sig : (Type -> Type) -> (Type -> Type))
  8 |          -> Type
  9 |          -> Type where
 10 |   Return : a -> Free sig a
 11 |   Op : sig (Free sig) a -> Free sig a
 12 | 
 13 | public export
 14 | Syntax sig => Functor (Free sig) where
 15 |   map f (Return x) = Return (f x)
 16 |   map f (Op op)    = Op (emap (map f) op)
 17 | 
 18 | public export
 19 | Syntax sig => Applicative (Free sig) where
 20 |   pure v = Return v
 21 | 
 22 |   Return v <*> prog = map v prog
 23 |   Op op    <*> prog = Op (emap (<*> prog) op)
 24 | 
 25 | public export covering
 26 | Syntax sig => Monad (Free sig) where
 27 |   Return v >>= prog = prog v
 28 |   Op op    >>= prog = Op (emap (>>= prog) op)
 29 | 
 30 | public export
 31 | return : a -> Free sig a
 32 | return = Return
 33 | 
 34 | public export
 35 | inject : Inj sub sup => sub (Free sup) a -> Free sup a
 36 | inject = Op . inj
 37 | 
 38 | public export
 39 | project : Prj sup sub => Free sup a -> Maybe (sub (Free sup) a)
 40 | project (Op s) = Just (prj s)
 41 | project _ = Nothing
 42 | 
 43 |