eff.lean

def {u} run_state {σ : Type u} (m : Type u → Type u) {n n' : Type u → Type u} {α : Type u} [monad_functor_t (state_t σ m) m n n'] [monad n] [monad_state σ n] [monad m]
  (x : n α) (st : σ) : n' (α × σ) :=
monad_map (λ α (x : state_t σ m α), prod.fst <$> x.run st) (prod.mk <$> x <*> get)

def {u} run_reader {ρ : Type u} (m : Type u → Type u) {n n' : Type u → Type u} {α : Type u} [monad_functor_t (reader_t ρ m) m n n'] [monad n] [monad_reader ρ n] [monad m]
  (x : n α) (env : ρ) : n' α :=
monad_map (λ α (x : reader_t ρ m α), x.run env) x

structure eff_types :=
(ε : option Type := none)
(ρ : option Type := none)
(σ : option Type := none)

def eff (c : eff_types := {}) : Type → Type :=
match c.ε, c.ρ, c.σ with
| some ε, some ρ, some σ := except_t ε (reader_t ρ (state σ))
| none,   some ρ, some σ := reader_t ρ (state σ)
| some ε, none,   some σ := except_t ε (state σ)
| none,   none,   some σ := state σ
| some ε, some ρ, none   := except_t ε (reader ρ)
| none,   some ρ, none   := reader ρ
| some ε, none,   none   := except_t ε id
| none,   none,   none   := id
end

section
local attribute [reducible] eff eff._match_1 lift_t coe_t coe

instance : Π (t : eff_types), monad (eff t)
| {ε := none, ρ := none, σ := none}       := infer_instance
| {ε := none, ρ := none, σ := some σ}     := infer_instance
| {ε := none, ρ := some ρ, σ := none}     := infer_instance
| {ε := none, ρ := some ρ, σ := some σ}   := infer_instance
| {ε := some ε, ρ := none, σ := none}     := infer_instance
| {ε := some ε, ρ := none, σ := some σ}   := infer_instance
| {ε := some ε, ρ := some ρ, σ := none}   := infer_instance
| {ε := some ε, ρ := some ρ, σ := some σ} := infer_instance

instance r1 (ε ρ σ : Type) : monad_reader ρ (eff {ε := ε, ρ := ρ, σ := σ}) := infer_instance
instance r2 (ρ σ : Type)   : monad_reader ρ (eff {ρ := ρ, σ := σ})         := infer_instance
instance r3 (ε ρ : Type)   : monad_reader ρ (eff {ε := ε, ρ := ρ})         := infer_instance
instance r4 (ρ : Type)     : monad_reader ρ (eff {ρ := ρ})                 := infer_instance

instance s1 (ε ρ σ : Type) : monad_state σ (eff {ε := ε, ρ := ρ, σ := σ})  := infer_instance
instance s2 (ε σ : Type)   : monad_state σ (eff {ε := ε, σ := σ})          := infer_instance
instance s3 (ρ σ : Type)   : monad_state σ (eff {ρ := ρ, σ := σ})          := infer_instance
instance s4 (σ : Type)     : monad_state σ (eff {σ := σ})                  := infer_instance

instance e1 (ε ρ σ : Type) : monad_except ε (eff {ε := ε, ρ := ρ, σ := σ}) := infer_instance
instance e2 (ε σ : Type)   : monad_except ε (eff {ε := ε, σ := σ})         := infer_instance
instance e3 (ε ρ : Type)   : monad_except ε (eff {ε := ε, ρ := ρ})         := infer_instance
instance e4 (ε : Type)     : monad_except ε (eff {ε := ε})                 := infer_instance

instance ra1 (ε ρ ρ' σ : Type) : monad_reader_adapter ρ ρ' (eff {ε := ε, ρ := ρ, σ := σ}) (eff {ε := ε, ρ := ρ', σ := σ}) := infer_instance
instance ra2 (ε ρ ρ' : Type)   : monad_reader_adapter ρ ρ' (eff {ε := ε, ρ := ρ}) (eff {ε := ε, ρ := ρ'}) := infer_instance
instance ra3 (ρ ρ' σ : Type)   : monad_reader_adapter ρ ρ' (eff {ρ := ρ, σ := σ}) (eff {ρ := ρ', σ := σ}) := infer_instance
instance ra4 (ρ ρ' σ : Type)   : monad_reader_adapter ρ ρ' (eff {ρ := ρ}) (eff {ρ := ρ'}) := infer_instance

instance sa1 (ε ρ σ σ' : Type) : monad_state_adapter σ σ' (eff {ε := ε, ρ := ρ, σ := σ}) (eff {ε := ε, ρ := ρ, σ := σ'}) := infer_instance
instance sa2 (ε σ σ' : Type)   : monad_state_adapter σ σ' (eff {ε := ε, σ := σ}) (eff {ε := ε, σ := σ'}) := infer_instance
instance sa3 (ρ σ σ' : Type)   : monad_state_adapter σ σ' (eff {ρ := ρ, σ := σ}) (eff {ρ := ρ, σ := σ'}) := infer_instance
instance sa4 (σ σ' : Type)     : monad_state_adapter σ σ' (eff {σ := σ}) (eff {σ := σ'}) := infer_instance

instance ea1 (ε ε' ρ σ : Type) : monad_except_adapter ε ε' (eff {ε := ε, ρ := ρ, σ := σ}) (eff {ε := ε', ρ := ρ, σ := σ}) := infer_instance
instance ea2 (ε ε' σ : Type)   : monad_except_adapter ε ε' (eff {ε := ε, σ := σ}) (eff {ε := ε', σ := σ}) := infer_instance
instance ea3 (ε ε' ρ : Type)   : monad_except_adapter ε ε' (eff {ε := ε, ρ := ρ}) (eff {ε := ε', ρ := ρ}) := infer_instance
instance ea4 (ε ε' ρ : Type)   : monad_except_adapter ε ε' (eff {ε := ε}) (eff {ε := ε'}) := infer_instance

/- We can add coercions for using exception free code into contexts with exception support. -/
instance c1 {σ ε ρ α : Type} : has_coe (eff {σ := σ, ρ := ρ} α) (eff {σ := σ, ρ := ρ, ε := ε} α) := ⟨λ a, except_t.lift a⟩
instance c2 {σ ε α : Type}   : has_coe (eff {σ := σ} α) (eff {σ := σ, ε := ε} α)                 := ⟨λ a, except_t.lift a⟩
instance c3 {ε ρ α : Type}   : has_coe (eff {ρ := ρ} α) (eff {ρ := ρ, ε := ε} α)                 := ⟨λ a, except_t.lift a⟩


@[inline] def using_state {α σ : Type} {t : eff_types} (s : σ) : eff {σ := σ, ..t} α → eff t α :=
match t with
| {ε := some ε, ρ := some ρ, σ := some σ'} := λ a, adapt_state (λ o, (s, o)) (λ s o, o) a
| {ε := some ε, ρ := some ρ, σ := none   } := λ a, do (r, _) ← run_state id a s, return r
| {ε := some ε, ρ := none, σ := some σ'}   := λ a, adapt_state (λ o, (s, o)) (λ s o, o) a
| {ε := some ε, ρ := none, σ := none}      := λ a, do (r, _) ← run_state id a s, return r
| {ε := none, ρ := some ρ, σ := some σ'}   := λ a, adapt_state (λ o, (s, o)) (λ s o, o) a
| {ε := none, ρ := some ρ, σ := none   }   := λ a, do (r, _) ← run_state id a s, return r
| {ε := none, ρ := none, σ := some σ'}     := λ a, adapt_state (λ o, (s, o)) (λ s o, o) a
| {ε := none, ρ := none, σ := none}        := λ a, do (r, _) ← run_state id a s, return r
end

@[inline] def using_reader {α ρ : Type} {t : eff_types} (r : ρ) : eff {ρ := ρ, ..t} α → eff t α :=
match t with
| {ε := some ε, ρ := some ρ, σ := some σ'} := λ a, adapt_reader (λ o, r) a
| {ε := some ε, ρ := some ρ, σ := none   } := λ a, adapt_reader (λ o, r) a
| {ε := some ε, ρ := none, σ := some σ'}   := λ a, ⟨⟨λ s, (a.run.run r).run s⟩⟩
| {ε := some ε, ρ := none, σ := none}      := λ a, ⟨a.run.run r⟩
| {ε := none, ρ := some ρ, σ := some σ'}   := λ a, adapt_reader (λ o, r) a
| {ε := none, ρ := some ρ, σ := none   }   := λ a, adapt_reader (λ o, r) a
| {ε := none, ρ := none, σ := some σ'}     := λ a, do s ← get, let (v, _) := (a.run r).run s, return v
| {ε := none, ρ := none, σ := none}        := λ a, a.run r
end

end