
  0 | module Control.EffectAlgebra
  1 | 
  2 | import public Control.HigherOrder
  3 | import public Control.Effect.Misc
  4 | 
  5 | ||| Structure that dispatches an effect.
  6 | public export
  7 | interface Monad m => Algebra sig m | m where
  8 |   constructor MkAlgebra
  9 |   alg : (f : Functor ctx)
 10 |      => ctx ()
 11 |      -> Handler ctx n m
 12 |      -> sig n a
 13 |      -> m (ctx a)
 14 | 
 15 | ||| Apply an effect within a monadic context that supports it.
 16 | public export
 17 | send : Inj eff sig => Algebra sig m => eff m a -> m a
 18 | send eff = alg {ctx = id} () id (inj eff)
 19 |