Help with universe levels and Monads

Stream: new members

[Miguel Negrão]

Hi, I'm trying to port some code from Haskell to Lean, to try to do some proofs. I'm having a real hard time with Monads and universe levels. Can anyone help with this issue with universe levels in the step function?

inductive Cell (m : Type u → Type v) [Monad m] (a b : Type u) : Type (max (u+1) v) where
  | cell {s : Type u} : (s × (s → a → m (b × s))) → Cell m a b

def step {m : Type u → Type v} {a b : Type u} [Monad m] : Cell m a b →  a →  m (b × Cell m a b)
  | (Cell.cell (cellState, cellStep)), a => do
      let (b, cellState') ←  cellStep cellState a
      pure (b, Cell.cell (cellState', cellStep))

The universe levels in Cell were added to make it typecheck, but perhaps they are not correct.

The error is on the step function, at m (b × Cell m a b):

failed to solve universe constraint
  u =?= max ?u.35573 ?u.35574
while trying to unify
  Type u : Type (u + 1)
with
  Type (max u v (u + 1)) : Type (max (u + 1) ((max v (u + 1)) + 1))

[Reid Barton]

These kinds of types are tricky (also in math). Here's a possible assignment of universe levels that makes your example work out

inductive Cell (m : Type (u + 1) → Type (u + 1)) [Monad m] (a b : Type (u + 1)) : Type (u+1) where
  | cell {s : Type u} : (s × (s → a → m (b × s))) → Cell m a b

def step {m : Type (u + 1) → Type (u + 1)} {a b : Type (u + 1)} [Monad m] : Cell m a b → a → m (b × Cell m a b)
  | (Cell.cell (cellState, cellStep)), a => do
      let (b, cellState') ←  cellStep cellState a
      pure (b, Cell.cell (cellState', cellStep))

[Miguel Negrão]

Thanks ! I think I understood the trick with using u+1, and it works great for this function. Yes, it does look a lot harder in Lean than in Haskell...

[Kevin Buzzard]

The moment I start struggling with universes I just drop them all. Do you need them to verify your Haskell code?

[Reid Barton]

That's in part because your theorems are coming from a system that is hopefully consistent, rather than one that is by design inconsistent

[Miguel Negrão]

Kevin Buzzard disse:

The moment I start struggling with universes I just drop them all. Do you need them to verify your Haskell code?

If I drop the universes then there is an error...

inductive Cell2 [Monad m] (a b : Type) : Type where
  | cell : (s × (s → a → m (b × s))) → Cell m a b

application type mismatch
  Cell m a
argument
  a
has type
  Type : Type 1
but is expected to have type
  Type (?u.39413 + 1) : Type (?u.39413 + 2)

[Yaël Dillies]

And what if you replace Type by Type*?

[Miguel Negrão]

Reid Barton disse:

That's in part because your theorems are coming from a system that is hopefully consistent, rather than one that is by design inconsistent

Agreed, there is a price to pay for consistency, but then you can prove statements.

With the solution above it seems I can't make a simple cell which receives nats and outputs nats. The universes again give an error:

def sumC [Monad m] : Cell m Nat Nat :=
  Cell.cell (0, (λ accum a => pure (accum, accum + a)))

application type mismatch
  Cell m Nat
argument
  Nat
has type
  Type : Type 1
but is expected to have type
  Type (?u.38017 + 1) : Type (?u.38017 + 2)

[Miguel Negrão]

Yaël Dillies disse:

And what if you replace Type by Type*?

That gives me an error, it thinks it's multiplication:

inductive Cell2 [Monad m] (a b : Type*) : Type* where
  | cell : (s × (s → a → m (b × s))) → Cell m a b

expected term

[Yaël Dillies]

Ah sorry you're on Lean 4. Replace Type with Type _.

[Yaël Dillies]

But also know that you truncated the error message right before the juicy bit.

[Miguel Negrão]

Yaël Dillies disse:

Ah sorry you're on Lean 4. Replace Type with Type _.

Right, I'm using lean 4.

inductive Cell2 [Monad m] (a b : Type _) : Type _ where
  | cell : (s × (s → a → m (b × s))) → Cell m a b

error:
unexpected constructor resulting type
  Cell m a b

Actually I really only got that output nothing else on the previous example. I'm using vscode, and that is what appears on the info pane.

[Yaël Dillies]

Why use inductive instead of structure, by the way? Your inductive type has only one non-recursive constructor.

[Miguel Negrão]

It will have another constructor (for efficiency) later, but for now I was only testing one constructor.

[Miguel Negrão]

inductive Cell2 [Monad m] (a b : Type _) : Type _ where
  | cell : (s × (s → a → m (b × s))) → Cell m a b
  | arrm : (a → m b) → Cell m a b

[Miguel Negrão]

What I'm doing is somewhat related to Kleisli categories. One constructor is a pure kleisli category, the other one is slightly altered with explicit state for livecoding in Haskell. The cell constructor is equivalent to product of state s with kleisli arrow a -> StateT s m b.

[Miguel Negrão]

The Haskell code is this: https://github.com/turion/essence-of-live-coding

[Alex J. Best]

One issue is you now have Cell and Cell2, and that m is now implicit I guess

inductive Cell2 [Monad m] (a b : Type _) : Type _ where
  | cell : (s × (s → a → m (b × s))) → Cell2 a b

[Miguel Negrão]

Ah, yes, thanks.

So correcting that, Cell works, but then I get a different problem with any use of Cell:

inductive Cell [Monad m] (m : Type _ → Type _) (a b : Type _) : Type _ where
  | cell : (s × (s → a → m (b × s))) → Cell m a b
  | arrm : (a → m b) → Cell m a b

def sumC [Monad m] {m : Type _ → Type _}: Cell m Nat Nat :=
  Cell.cell (0, (λ accum a => pure (accum, accum + a)))

Problem is in Cell m Nat Nat

Main.lean:194:50
Expected type
m✝: Type ?u.36143 → Type ?u.36142
inst✝: Monad m✝
m: Type → Type ?u.36150
⊢ Type
Messages (1)
Main.lean:194:43

typeclass instance problem is stuck, it is often due to metavariables
  Monad ?m.36159

[Alex J. Best]

The argument m needs to be before [Moand m] if you look carefully at the error message you'll see you have two m's now and only the first one is a monad

[Miguel Negrão]

Ah, got it, so the type class constraint should come after the arguments that it refers to (sorry for newbiness... :smiling_face: ). This gets me a bit further, sumC now works. Then I get stuck in the code for evaluating a cell:

inductive Cell (m : Type _ → Type _) [Monad m] (a b : Type _) : Type _ where
  | cell : (s × (s → a → m (b × s))) → Cell m a b
  | arrm : (a → m b) → Cell m a b

def sumC {m : Type _ → Type _} [Monad m]: Cell m Nat Nat :=
  Cell.cell (0, (λ accum a => pure (accum, accum + a)))

def step {m : Type _ → Type _} [Monad m] : Cell m a b → a → m (b × Cell m a b)
  | Cell.cell (cellState, cellStep), a => do
      let (b, cellState') ←  cellStep cellState a
      pure (b, Cell.cell (cellState', cellStep))
  | Cell.arrm f, a => (λ x => (x , cell)) <$> f a

The error is in the type of step

Main.lean:197:0
Messages (2)
Main.lean:197:0

stuck at solving universe constraint
  max ?u.36246 ?u.36247 =?= max ?u.36228 ?u.36229
while trying to unify
  (Type (max ?u.36247 ?u.36246) → Type ?u.36215) →
    Type ?u.36215 : Type (max (max (?u.36215 + 1) (?u.36246 + 1)) (?u.36247 + 1))
with
  (Type (max ?u.36228 ?u.36229) → Type ?u.36215) →
    Type ?u.36215 : Type (max (max (?u.36215 + 1) (?u.36228 + 1)) (?u.36229 + 1))

Main.lean:197:0

stuck at solving universe constraint
  max
  (?u.36228+1)
  (?u.36229+1) =?= max (max (max (max (?u.36215+1) (?u.36226+1)) (?u.36228+1)) (?u.36229+1)) (?u.36246+2)
while trying to unify
  Type (max ?u.36228 ?u.36229) : Type ((max ?u.36228 ?u.36229) + 1)
with
  Type
    (max (max ?u.36228 ?u.36229) (max ?u.36226 ?u.36215)
        (?u.36246 + 1)) : Type (max ((max ?u.36228 ?u.36229) + 1) ((max (max ?u.36226 ?u.36215) (?u.36246 + 1)) + 1))

[Alex J. Best]

Did you try Reid's version again? with explicit universes

[Miguel Negrão]

With that version, step works, but not sumC, with the following error:

inductive Cell (m : Type (u + 1) → Type (u + 1)) [Monad m] (a b : Type (u + 1)) : Type (u+1) where
  | cell {s : Type u} : (s × (s → a → m (b × s))) → Cell m a b
  | arrm : (a → m b) → Cell m a b

def sumC {m : Type _ → Type _} [Monad m]: Cell m Nat Nat :=
  Cell.cell (0, (λ accum a => pure (accum, accum + a)))

Main.lean:194:50
Expected type
m: Type 1 → Type 1
inst✝: Monad m
⊢ Type 1
Messages (1)
Main.lean:194:49

application type mismatch
  Cell m Nat
argument
  Nat
has type
  Type : Type 1
but is expected to have type
  Type (?u.35827 + 1) : Type (?u.35827 + 2)

[Gary Haussmann]

The problem here is that Nat (along with most simple datatypes) is explicitly declared as Type 0 so it won't fit into places where you need a Type 1 or Type (u+1). You can use ULift to move types between universes, in this case we pop Nat up into universe u+1:

inductive Cell (m : Type (u + 1) → Type (u + 1)) [Monad m] (a b : Type (u + 1)) : Type (u+1) where
  | cell {s : Type u} : (s × (s → a → m (b × s))) → Cell m a b
  | arrm : (a → m b) → Cell m a b

def sumC {m : Type _ → Type _} [Monad m]: Cell m (ULift Nat) (ULift Nat) :=
  Cell.cell (0, (λ accum a => pure (ULift.up accum, accum + ULift.down a)))

Note that in sumC you need to use ULift.down to drop back down to universe 0 and pull out the original Nat.
This works, but feels kind of clunky. You could also make a custom version of Nat that is of Type u, or maybe there is one already written up somewhere?

[Gary Haussmann]

Also if I'm at the point where I'm pulling out ULift I usually go back and see if I can rewrite the relevant data/functions to avoid all this universe manipulation. However if you need Cell and step to be the way they are then you're probably stuck with ULift

[Miguel Negrão]

@Gary Haussmann thank you much ! With ULift indeed I can get it to compile. At the moment I don't know enough about universes to see how to write Cell and step any other way (while compiling), so I guess I'll stick with this solution. I'm having some issues with ULift though. It seems I can't use it with <$> (also called fmap or map perhaps ? ).

inductive Cell (m : Type (u + 1) → Type (u + 1)) [Monad m] (a b : Type (u + 1)) : Type (u+1) where
  | cell {s : Type u} : (s × (s → a → m (b × s))) → Cell m a b
  | arrm : (a → m b) → Cell m a b

def sumC {m : Type _ → Type _} [Monad m]: Cell m (ULift Nat) (ULift Nat) :=
  Cell.cell (0, (λ accum a => pure (ULift.up accum, accum + ULift.down a)))

def step {m : Type _ → Type _} [Monad m] : Cell m a b → a → m (b × Cell m a b)
  | Cell.cell (cellState, cellStep), a => do
      let (b, cellState') ←  cellStep cellState a
      pure (b, Cell.cell (cellState', cellStep))
  | Cell.arrm f, a => (λ x => (x , Cell.arrm f)) <$> f a

def steps  {m : Type _ → Type _} [Monad m] : Cell m a b → List a → m (List b × Cell m a b)
  | cell, []        => pure ([], cell)
  | cell, (a :: as) => do
    let (b, cell') ←  step cell a
    let (bs, cell'') ←  steps cell' as
    pure (b :: bs, cell'')

#eval Prod.fst $ Id.run $ step sumC (ULift.up (0:Nat))

#eval Prod.fst $ Id.run $ steps sumC [ULift.up (1:Nat), ULift.up (1:Nat), ULift.up (1:Nat)]
-- evaluates to:
-- [ULift.up 0, ULift.up 1, ULift.up 2]

-- Erro here:
#eval Id.run steps sumC (ULift.up <$> ([1, 1, 1] : List Nat))

Main.lean:217:61
Expected type
⊢ List (ULift Nat)
Messages (1)
Main.lean:217:38
application type mismatch
  ?m.45690 <$> [1, 1, 1]
argument
  [1, 1, 1]
has type
  List Nat : Type
but is expected to have type
  List ?m.45650 : Type 1
` ``

[Miguel Negrão]

In any case, this already allows me to go on to try to prove some theorems. Thanks so much to everyone that helped !