Effect System

Monadic Effect Handlers

Effects

Programming effect system with single Monad and Effect Handlers.

Effect

record effect (v:Type) (r:Type): Type := (values: v) (resource: r) (computation: (v → r)) (handler: effect v r → monad effect v r) data RA: Type := (intro: effect nat (random nat)) data IO (t:Type): Type := (intro: effect t (file t)) data EX (t:Type): Type := (intro: effect () (exception t))

Eff.Monad

data Eff.Monad (eff: list effect) (m: Type → Type) (a: Type): Type := (intro: eff m a xs (\ (v: Type) → xs) → monad_eff xs m a)

Eff.Handler

record Eff.Handler (e: effect) (m: Type → Type): Type := (action: ∀ (r: res) (eff: e t res resk) (k: ∀ (x: t) → resk x → m a) → m a)