wish_list.lean

import system.io

variables {δ ε ρ σ α : Type}
/-
- δ : backtrackable state
- ε : exception type
- ρ : environment
- σ : non backtrackable state
-/

def eff_core (effs : list ((Type → Type) → Type → Type)) (b : Type → Type) : Type → Type :=
effs.foldr ($) b

def eff (effs : list ((Type → Type) → Type → Type)) : Type → Type :=
eff_core effs id

def eff_io (effs : list ((Type → Type) → Type → Type)) : Type → Type :=
eff_core effs io

-- Most of the time we want to use substacks of the following two monads
#check eff [state_t δ, except_t ε, reader_t ρ, state_t σ]
#check eff_io [state_t δ, except_t ε, reader_t ρ, state_t σ]

/-
1) We want to be able to add "more effects".
It would be great if we could have a single "polymorphic" `using_reader` adapter that
would conver cases such as:
-/
constant using_reader₁ (r : ρ) (a : eff [except_t ε, state_t σ] α) : eff [except_t ε, reader_t ρ, state_t σ] α
constant using_reader₂ (r : ρ) (a : eff [state_t δ, except_t ε, state_t σ] α) : eff [state_t δ, except_t ε, reader_t ρ, state_t σ] α
-- ..
/- Same for `using_state` (non-backtrackable) and `using_bstate` (backtrackable) -/
constant using_state₁ (r : ρ) (a : eff [except_t ε] α) : eff [except_t ε, state_t σ] α
constant using_state₂ (r : ρ) (a : eff [except_t ε, reader_t ρ] α) : eff [except_t ε, reader_t ρ, state_t σ] α
-- ...
constant using_bstate₁ (r : ρ) (a : eff [except_t ε] α) : eff [state_t δ, except_t ε] α
-- ...
/- I don't know how to implement this using the `effs.foldr` encoding or explicit monad stacks.
   It seems the best option in this case is to use `run_state/run_reader/...`.
   However, if we have two different states, it is not clear to me how to use `run_state`. -/

local attribute [reducible] eff eff_core list.foldr
/-
2) We want to lift actions automatically. 
We can use `monad_lift` manually to conveniently add new effects on the top of the stack.
-/
def bla1 (a : eff [state_t σ] α) : eff [except_t ε, reader_t ρ, state_t σ] α :=
monad_lift a

/- We can use coercions to insert `monad_lift` automatically in specific cases. -/
instance c1 : has_coe (eff [reader_t ρ, state_t σ] α) (eff [except_t ε, reader_t ρ, state_t σ] α) :=
⟨λ a, monad_lift a⟩

/- However, we need to add an instance for each pair of configurations. -/

/- I don't know any convenient way of adding effects in the middle of stack. -/
def bla2 (a : eff [except_t ε, state_t σ] α) : eff [except_t ε, reader_t ρ, state_t σ] α :=
monad_lift a -- doesn't work

/- I only know how to do it case-by-case. 
   For each special case we can add a coercion for applying the lift automatically.
-/

/-
3) We want to adapt state/reader/exceptions.
We can do this in all encodings by using the functions `adapt_state`, `adapt_reader`, ...
-/

/-
4) We want to access the two different states in a convenient way.
It would be great if we could use `get/put` for non-backtrackable state, and
`getδ/putδ` for backtrackable state.

Right now, if we have both [state_t δ, ..., state_t σ], `get/put` access the
backtrackable state δ. I tried to use `v : σ ← get` to access the non-backtrackable
one, but it doesn't work.
-/
def foo1 : state_t δ (state_t σ id) σ :=
monad_lift (get : state_t σ id σ) -- doesn't work

def foo2 : state_t δ (state_t σ id) σ :=
do s ← monad_lift (get : state_t σ id σ), -- works
   return s

def foo3 : state_t δ (state_t σ id) σ :=
do s ← monad_lift get, -- doesn't work
   return s

def foo4 : eff [state_t δ, except_t ε, reader_t ρ, state_t σ] σ :=
monad_lift (get : eff [except_t ε, reader_t ρ, state_t σ] σ) -- doesn't work

def foo5 : eff [state_t δ, except_t ε, reader_t ρ, state_t σ] σ :=
do s ← monad_lift (get : eff [except_t ε, reader_t ρ, state_t σ] σ), -- works
   return s

/- 
- foo2 and foo5 work, but it is really annoying to use the type ascryption. 
- I don't know why foo1 and foo4 do not work.
-/


/-
5) (minor) With `effs.foldr` or explicit monad stacks, I don't know
how to enforce an uniform representation. For example, in one file
we may define
-/
def act1 : eff [except_t ε, state_t σ, reader_t ρ] unit :=
-- ...
return ()
/- and in another file -/
def act2 : eff [except_t ε, reader_t ρ, state_t σ] unit :=
-- ...
return ()
/- They are morally compatible, but we can't easily combine them. -/
def boo1 : eff [except_t ε, reader_t ρ, state_t σ] unit :=
act1 >> act2 -- Error
/- The `eff` approach at eff.lean solves this problem. 
   It also prevents mistakes. For example, in the following
   example both states are non backtrackable. -/
def boo2 : eff [except_t ε, state_t δ, reader_t ρ, state_t σ] unit :=
-- ...
return ()