Lost in the multiverse ...

Stream: lean4

[Yuri de Wit]

I am having some difficulties translating code from Idris 2 to Lean 4 with respect to universes.

I understand the notion of a tower of universes starting with Type, i.e. Type 0and I thought I understood the notion of a universe bump when mixing different universes in the same type constructor (i.e. #check Prod -- Type u_1 → Type u_2 → Type (max u_1 u_2)). However, I am having a hard time putting it to practice.

Could someone help?

/-
interface ReadContext context where
  getRead : context -> Type
  setRead : Type -> context -> context
  getSetId : {0 ctx : context} -> getRead (setRead a ctx) = a

[ReadPair] ReadContext (Type, List (String, Type)) where
  getRead (a, env) = a
  setRead r (a, env) = (r, env)
  getSetId {ctx = (a, env)} = Refl
-/

This is my attempt:

class ReadContext (context : Type u) where
  getRead : context -> Type
  setRead : Type -> context -> context
  getSetId : {ctx : context} -> getRead (setRead a ctx) = a

instance readPair : ReadContext (a : Type × List (String × Type)) -> Type where
  getRead (Prod a _) := a
  setRead r (Prod a env) := (r, env)
  -- getSetId {ctx = (a, env)} = Refl

Here is the error I get:

application type mismatch
  ReadContext a
argument
  a
has type
  Type × List (String × Type) : Type 1  --- this makes sense :
but is expected to have type
  Type ?u.409 : Type (?u.409 + 1)

[Sebastian Ullrich]

Hmm, why did you add the a :? The problem is not universes, but that you're passing a value (a) where a type was expected. A direct translation works.

instance readPair : ReadContext (Type × List (String × Type)) where

[Yuri de Wit]

Ooh, I see the stupidity now ... I was thinking that a was just a name for (Type × List (String × Type)), but I am actually instantiating ReadContext with a value of this type!

[Yuri de Wit]

Let me try to get the example working. I think I have another follow up question.

[Yuri de Wit]

I could get this to work:

class ReadContext (context : Type u) where
  getRead : context -> Type v
  setRead : Type v -> context -> context
  getSetId : {ctx : context} -> getRead (setRead a ctx) = a

instance readPair : ReadContext (Type × List (String × Type)) where
  getRead | Prod.mk a _ => a
  setRead | r, (Prod.mk _ env) => Prod.mk r env
  getSetId := sorry -- TODO

However, I was stuck for a while trying to figure why the following was not working:

  setRead | r, (Prod.mk _ env) => (r × env) -- error in second 'env'

Here is the error:

application type mismatch
  r × env
argument
  env
has type
  List (String × Type) : Type 1
but is expected to have type
  Type ?u.538 : Type (?u.538 + 1)

Why does it work with Prod.mk but not with ×?

[Henrik Böving]

the \times is notation for the type Prod while Prod.mk is the constructor, if you want to match on a thing of type Prod you have to match on (x, y)

[Yuri de Wit]

Interesting ... but isn't (Nat × String) a notation for (Prod.mk Nat String)? I was assuming they were interchangeable.

[Henrik Böving]

No that's notation for Prod Nat String

[Henrik Böving]

(x, y) = Prod.mk x y, (x × y) = Prod x y where the first one is an actualy value of type Prod and the second one is the type Prod x y

[Yuri de Wit]

So obvious now ... and the source of many of my struggles!

Thank you @Henrik Böving and @Sebastian Ullrich !

[Sebastian Ullrich]

It certainly doesn't help that Idris reuses the same notation for both levels :)

[Yuri de Wit]

One last question ...

class ReadContext (context : Type u) where
  getRead : context -> Type v
  setRead : Type v -> context -> context
  getSetId : {ctx : context} -> getRead (setRead a ctx) = a

getSetId is a law that must hold for all instances of this class, right? How do I implement this? The Idris2 source implements it with getSetId {ctx = (a, env)} = Refl.

(feel free to point me to reading material ... this is uncharted territory for me)

[Henrik Böving]

So what idris is doing here ( I think I dont know idris) is to set a default value for the field, you can do this in Lean as well by doing: := ... at the end of your field notation, in this case := by rfl. If the rfl proof does not work out (or the user wants to choose another one for another reason) they can overwrite this while creating their instance by simply assigning a value to the field as per usual...I dont know whether this is documented anywhere.

[Henrik Böving]

Ah no they are not doing a default alue they are doing it in the instance I didnt read the code above.

[Henrik Böving]

What i said still applies though^^

[Sebastian Ullrich]

The closest translation would be getSetId := @fun _ (a, env) => rfl. {ctx = is a named parameter, but Lean only supports them for applications, not definitions.

[Yuri de Wit]

Sebastian Ullrich said:

The closest translation would be getSetId := @fun _ (a, env) => rfl. {ctx = is a named parameter, but Lean only supports them for applications, not definitions.

I see. So ctx is not visible in the implementation and you are binding it to _ and (a,env)using a lambda so it can be used for the proof.

[Sebastian Ullrich]

The _ is the implicitly bound a from the declaration of ReadContext.getSetId. The name reuse is a bit confusing (again).

[Yuri de Wit]

I need to rely more on the infoView to help go through this. E.g. getSetId := rfl will show me:

a✝ : Type
ctx✝ : Type × List (String × Type)
⊢ (fun x =>
      match x with
      | (a, snd) => a)
    ((fun x x_1 =>
        match x, x_1 with
        | r, (fst, env) => (r, env))
      a✝ ctx✝) =
  a✝

I am assuming that ✝ is a marker for an inaccessible binding?

In any case, I think I am getting ahead of myself here. For now, let me finish the complete translation fro Idris2 and see if I fully grok it.

[Yuri de Wit]

Thanks again!