BaseIO, IO, and monad transformers

Stream: general

[James Sully]

I recently refactored my program to use a reader. I've been running into an issue where BaseIO somehow automatically converts to IO no problem, but when I wrap them in my transformer, they're not directly compatible.
Simplified:

def CmdHandlerEnv := Unit
abbrev CmdHandlerT (m : Type → Type) : Type → Type := ReaderT CmdHandlerEnv m

def baseIOAction : BaseIO Unit := pure ()
-- ok
example : IO Unit := baseIOAction

def transformedBaseIOAction : CmdHandlerT BaseIO Unit := pure ()
/-
type mismatch
  transformedBaseIOAction
has type
  CmdHandlerT BaseIO Unit : Type
but is expected to have type
  CmdHandlerT IO Unit : Type
-/
example : CmdHandlerT IO Unit := transformedBaseIOAction

I can work around it like this:

instance : Coe (ReaderT ρ BaseIO α) (ReaderT ρ IO α) where
  coe act := λ r ↦ (act.run r).toIO

But this feels kind of janky and specific

My questions are

• what's the mechanism by which BaseIO is converted to IO automatically? I can't find a Coe instance.
• Is there a better way to do this?
• could that better way be done generically in the standard library for every transformer?

[Edward van de Meent]

if instead of example you use def foo : IO Unit := baseIOAction, you can use #print to discover what's going on in the conversion:

def CmdHandlerEnv := Unit
abbrev CmdHandlerT (m : Type → Type) : Type → Type := ReaderT CmdHandlerEnv m

def baseIOAction : BaseIO Unit := pure ()
-- ok
def foo : IO Unit := baseIOAction

#print foo -- def foo : IO Unit := @liftM BaseIO (EIO IO.Error) (instMonadLiftTOfMonadLift BaseIO BaseIO (EIO IO.Error)) Unit baseIOAction
--

basically, it seems like there is a Coe-like typeclass MonadLift saying you can lift BaseIO to IO.
you can check this by using #synth MonadLift BaseIO IO

[Edward van de Meent]

it seems to go through an intermediate class MonadLiftT but that looks to me like an implementation detail

[James Sully]

Thanks, I'll play around with this

[James Sully]

Ok I fumbled around in the dark a bit and got stuck:

instance {m n ω : Type → Type} {t : (Type → Type) → Type → Type} [MonadLift m n] [MonadLift ω (t ω)] : MonadLift (t m) (t n) := sorry

"cannot find synthesization order for instance @instMonadLift with type
{m n ω : Type → Type} →
{t : (Type → Type) → Type → Type} → [inst : MonadLift m n] → [inst : MonadLift ω (t ω)] → MonadLift (t m) (t n)
all remaining arguments have metavariables:
MonadLift ?ω (t ?ω)"

[James Sully]

I'm not really sure whether I have the right idea here or not

[Yaël Dillies]

Should {ω : Type → Type} [MonadLift ω (t ω)] instead be [∀ ω, MonadLift ω (t ω)]?

[James Sully]

Yes!

[James Sully]

instance {m n: Type → Type} {t : (Type → Type) → Type → Type} [MonadLift m n] [∀ ω, MonadLift ω (t ω)] : MonadLift (t m) (t n) where
  monadLift {α : Type} (action : (t m) α) : (t n) α :=
    sorry

[James Sully]

the next thing to figure out is how to implement it

[James Sully]

I haven't managed to figure it out in full generality (not even sure whether it's possible), but here's one for ReaderT

instance monadLiftReaderT [MonadLift m n] : MonadLift (ReaderT σ m) (ReaderT σ n) where
  monadLift action := λ r => liftM <| action.run r

Would this be a good addition to the standard library?

[Sebastian Ullrich]

I think such instances could be problematic when you stack the same transformer multiple times as now you get quadratically many possible instances

[James Sully]

It definitely feels like there's an ergonomics issue here, but I'm not sure what the right solution is

[James Sully]

what about just

instance : MonadLift (ReaderT σ BaseIO) (ReaderT σ IO) where
  monadLift action := λ r => liftM <| action.run r

[Sebastian Ullrich]

Feels quite ad-hoc :) . It's a fine local instance though.

[James Sully]

I agree it's ad hoc, but in the absence of a general solution, it feels like an 80/20 thing that would add a lot of convenience. Defining just a ReaderT σ IO is pretty common (at least in haskell).