IO with a type parameter in universe > 1

Stream: lean4

[Juan Pablo Romero]

Hi, I'm trying to create the following type:

universe u
inductive Wrapper : Type u -> Type (u + 1) where
  | Pure {A : Type u} (value: A) : Wrapper A
  | Effect {A : Type u} (io: IO A) : Wrapper A

which fails because IO has type Type → Type.

Is there a way to overcome this issue?

[Mauricio Collares]

Relevant: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/universe.20polymorphic.20IO

[Sébastien Michelland]

Which I should be able to look into again. I left it unfinished because of more pressing problems.

[Juan Pablo Romero]

I managed to make it work with liberal use of ULift

universe u
inductive Wrapper : Type u -> Type (u + 1) where
  | Pure {A : Type u} (value: A) : Wrapper A
  | Effect {A : Type} (io: ULift.{u} (IO A)) : Wrapper (ULift.{u} A)

def run {A: Type u} {B: Type} (w: Wrapper A) (next: A -> IO B) : IO B :=
  match w with
    | .Pure a =>
      next a

    | .Effect lio =>
      let io := ULift.down.{u} lio
      io.bind <| fun a => next (ULift.up.{u} a)

[Sébastien Michelland]

Right. If this is sufficient for your needs, then it's likely the best option. Note that compared to your original definition you are limited to computing in Type while in the IO monad. I might be wrong here, but this looks like a free(r) monad, and I believe this typing will make it hard for you to bind with effects. You can see how already your continuation is restricted to B: Type. If you want to use a B: Type v or simply a Wrapper B to continue the program, you will find yourself matching B against a universe lift of A: Type in the Effect constructor, so basically you're grounded at Type 0.

[Juan Pablo Romero]

It's good for now, thanks!