Monad Lifting

Stream: general

[Mai]

Why can't this automatically lift?

def foo : Option Nat := sorry
def bar : OptionT (StateM Nat) Nat := do
  let _ <- foo
  sorry

[Jakub Nowak]

Good question. There's ExceptT.instMonadLiftExcept but no lift for Option. Was it left on purpose or just was forgotten?

You can add it locally:

@[always_inline]
instance {m : Type u → Type v} [Monad m] : MonadLift Option (OptionT m) := ⟨fun e => OptionT.mk <| pure e⟩

def foo : Option Nat := do return 2
def bar : OptionT (StateM Nat) Nat := do
  let _ <- foo
  sorry

[Aaron Liu]

there's also docs#liftOption

[Mai]

Also, StateM Nat Nat doesn't seem to lift to StateT Nat Option Nat. Shouldn't it?

[Chris Henson]

Some earlier discussion here: #lean4 > `MonadLift Option (OptionT m)`

[Mai]

Would something like this make sense?

instance [Pure m] : MonadLift (StateM σ) (StateT σ m) where
  monadLift m := pure ∘ m

[Mai]

I am pretty sure Id lifts into any monad

[Mai]

Or even a more extreme generalization?

instance [MonadLift m n] : MonadLift (StateT σ m) (StateT σ n) where
  monadLift m σ := m σ

[Mai]

(The reasoning is that I would expect any automatic lifting in a do block to keep working after transforming the monad with StateT)

[Mai]

Oh no, Id isn't MonadLift, it's MonadLiftT... :cry:
Would this make sense?

instance [MonadLiftT m n] : MonadLiftT (StateT σ m) (StateT σ n) where
  monadLift m σ := m σ