eff2.lean

universes u

def eff (effs : list ((Type u → Type u) → Type u → Type u)) : Type u → Type u :=
effs.foldr ($) id

section
local attribute [reducible] eff list.foldr
variables {ε ρ σ : Type u}

instance eff.m1 : monad $ eff [except_t ε, reader_t ρ, state_t σ] := infer_instance
instance eff.m2 : monad $ eff [except_t ε, state_t σ] := infer_instance
instance eff.m3 : monad $ eff [state_t σ] := infer_instance
-- ...

instance eff.r1 : monad_reader ρ $ eff [except_t ε, reader_t ρ, state_t σ] := infer_instance
instance eff.r2 : monad_reader ρ $ eff [except_t ε, reader_t ρ] := infer_instance
instance eff.r3 : monad_reader ρ $ eff [reader_t ρ, state_t σ] := infer_instance
instance eff.r4 : monad_reader ρ $ eff [reader_t ρ] := infer_instance

instance eff.s1 : monad_state σ $ eff [except_t ε, reader_t ρ, state_t σ] := infer_instance
instance eff.s2 : monad_state σ $ eff [except_t ε, state_t σ] := infer_instance
instance eff.s3 : monad_state σ $ eff [reader_t ρ, state_t σ] := infer_instance
instance eff.s4 : monad_state σ $ eff [state_t σ] := infer_instance

instance eff.e1 : monad_except ε $ eff [except_t ε, reader_t ρ, state_t σ] := infer_instance
instance eff.e2 : monad_except ε $ eff [except_t ε, reader_t ρ] := infer_instance
instance eff.e3 : monad_except ε $ eff [except_t ε, state_t σ] := infer_instance
instance eff.e4 : monad_except ε $ eff [except_t ε] := infer_instance

instance c1 {σ ε ρ α : Type} : has_coe (eff [reader_t ρ, state_t σ] α) (eff [except_t ε, reader_t ρ, state_t σ] α) := ⟨λ a, except_t.lift a⟩
instance c2 {σ ε α : Type} : has_coe (eff [state_t σ] α) (eff [except_t ε, state_t σ] α) := ⟨λ a, except_t.lift a⟩
instance c3 {ε ρ α : Type} : has_coe (eff [reader_t ρ] α) (eff [except_t ε, reader_t ρ] α) := ⟨λ a, except_t.lift a⟩

instance ra1 (ε ρ ρ' σ : Type) : monad_reader_adapter ρ ρ' (eff [except_t ε, reader_t ρ, state_t σ]) (eff [except_t ε, reader_t ρ', state_t σ]) := infer_instance
instance ra2 (ρ ρ' σ : Type) : monad_reader_adapter ρ ρ' (eff [reader_t ρ, state_t σ]) (eff [reader_t ρ', state_t σ]) := infer_instance
instance ra3 (ε ρ ρ' : Type) : monad_reader_adapter ρ ρ' (eff [except_t ε, reader_t ρ]) (eff [except_t ε, reader_t ρ']) := infer_instance
instance ra4 (ε ρ ρ' : Type) : monad_reader_adapter ρ ρ' (eff [reader_t ρ]) (eff [reader_t ρ']) := infer_instance

instance sa1 (ε ρ σ σ' : Type) : monad_state_adapter σ σ' (eff [except_t ε, reader_t ρ, state_t σ]) (eff [except_t ε, reader_t ρ, state_t σ']) := infer_instance
instance sa2 (ε σ σ' : Type) : monad_state_adapter σ σ' (eff [except_t ε, state_t σ]) (eff [except_t ε, state_t σ']) := infer_instance

end