More universe level related issues #3

[refparo]

More universe level related issues #3

[ice1000]

Don't trust the route error messages, they're cursed. I'll try to improve it!

[ice1000]

It's not printing all equations, and the reason is that some equations are generated at overlapped source range, which are overwritten during printing.

[ice1000]

I asked you about mkVerb some time ago but you replied with a definition of Verb, saying that it's okay.

[ice1000]

#22

[refparo]

I asked you about mkVerb some time ago but you replied with a definition of Verb, saying that it's okay.

The code in #19 never included mkVerb, and I wasn't paying attention when you asked… Sorry.

[ice1000]

Have you seen Event.u <= Verb.v?

[refparo]

Yeah, and Verb.v == v, so I concluded that Event.u <= v.

[ice1000]

There is a way to do it, but it's gonna be very complicated, which is to introduce assumptions on level relations. I think that will require an overhaul of the level system.

[ice1000]

Yeah, and Verb.v == v, so I concluded that Event.u <= v.

And apparently Verb.v = v, and Event.u = u, so you're asking two parameters to have a relation. But we don't support that (say, take two level arguments with a known relation) at the moment.

[ice1000]

I mean you're asking u <= v. For now you can pass arbitrary level arguments so they should be independent

[refparo]

Yeah, I understand that. But after changing the type of mkVerb the code still doesn't tyck. I think the changed code doesn't involve any assumptions.

[ice1000]

Oh I didn't read the entire post. I'm running test now. Java compilation has become disastrously slow lately and I dunno why. Maybe it's the doom of this 5000RMB laptop...

[ice1000]

This is what I got:

         Verb.u == u
         Verb.v == (lmax u v)
         u <= Verb.u
         Event.u == u
         u <= Event.u
         Event.u <= Verb.v
         Event.u <= u
         (lmax u v) <= Verb.v
         Event.u <= Verb.u
         Verb.v <= Verb.v

[ice1000]

Still requiring v >= u, man.

[refparo]

It's Event.u <= Verb.v, but Event.u == u and Verb.v == lmax u v, so u <= lmax u v, which is obvious.

[ice1000]

With the latest commit you'll be able to see the complete list of level constraints

[ice1000]

Well I think you're right. This needs more investigation

[refparo]

My another failed attempt:

(The problem is also u <= (lmax u v))

universe u v

open data EventT : Type (lsuc u)
  | CarrierT (A : Type u)

def GetAgentT (T : EventT {universe u}) : Type u
  | CarrierT A => A

struct Event (T : EventT {universe u}) : Type u
  | agent : GetAgentT T

def Quantifier (A : Type (lsuc u)) : Type (lsuc (lmax u v))
  => (A -> Type v) -> Type (lmax u v)

def Verb (T : EventT {universe (lsuc u)}) : Type (lsuc (lmax u v))
  => Quantifier {universe u, v} (Event T)

def mkVerb {T : EventT {universe (lsuc u)}} (p : Event {universe (lsuc u)} T -> Type v)
  : Verb {universe u, v} T
  => \f => Sig (e : Event {universe (lsuc u)} T) (s : p e) ** (f e)

[refparo]

A minimum test:

The following tycks:

universe u v

open data Event : Type u

def Quantifier (A : Type (lsuc u)) : Type (lsuc (lmax u v))
  => (A -> Type v) -> Type (lmax u v)

def Verb : Type (lsuc (lmax u v))
  => Quantifier {universe u, v} Event

def mkVerb (p : Event {universe u} -> Type v)
  : Quantifier {universe u, v} Event
  => \f => Sig (e : Event {universe u}) (s : p e) ** (f e)

But this doesn't:

universe u v

open data Event : Type u

def Quantifier (A : Type (lsuc u)) : Type (lsuc (lmax u v))
  => (A -> Type v) -> Type (lmax u v)

def Verb : Type (lsuc (lmax u v))
  => Quantifier {universe u, v} Event

def mkVerb (p : Event {universe u} -> Type v)
  : Verb {universe u, v}
  => \f => Sig (e : Event {universe u}) (s : p e) ** (f e)

[ice1000]

Later we should test against all these

[refparo]

This extra explicit universe level would fix the failing code in #57 (comment) :

 universe u v

 open data Event : Type u

 def Quantifier (A : Type (lsuc u)) : Type (lsuc (lmax u v))
   => (A -> Type v) -> Type (lmax u v)

 def Verb : Type (lsuc (lmax u v))
-  => Quantifier {universe u, v} Event
+  => Quantifier {universe u, v} (Event {universe u})

 def mkVerb (p : Event {universe u} -> Type v)
   : Verb {universe u, v}
   => \f => Sig (e : Event {universe u}) (s : p e) ** (f e)

[refparo]

The universe annotation in #57 (comment) actually has some errors, which should be fixed as follows:

 universe u v

 open data EventT : Type (lsuc u)
   | CarrierT (A : Type u)

 def GetAgentT (T : EventT {universe u}) : Type u
   | CarrierT A => A

 struct Event (T : EventT {universe u}) : Type u
   | agent : GetAgentT T

 def Quantifier (A : Type (lsuc u)) : Type (lsuc (lmax u v))
   => (A -> Type v) -> Type (lmax u v)

-def Verb (T : EventT {universe (lsuc u)}) : Type (lsuc (lmax u v))
+def Verb (T : EventT {universe u}) : Type (lsuc (lmax u v))
   => Quantifier {universe u, v} (Event T)

-def mkVerb {T : EventT {universe (lsuc u)}} (p : Event {universe (lsuc u)} T -> Type v)
+def mkVerb {T : EventT {universe u}} (p : Event {universe u} T -> Type v)
   : Verb {universe u, v} T
-  => \f => Sig (e : Event {universe (lsuc u)} T) (s : p e) ** (f e)
+  => \f => Sig (e : Event {universe u} T) (s : p e) ** (f e)

It's my fault, sorry.

[refparo]

Strangely, removing some universe annotation would make the original code tyck:

 universe u v

 open data EventT : Type (lsuc u)
   | CarrierT (A : Type u)

 def GetAgentT (T : EventT {universe u}) : Type u
   | CarrierT A => A

 struct Event (T : EventT {universe u}) : Type u
   | agent : GetAgentT T

 def Quantifier (A : Type u) : Type (lmax u (lsuc v)) => (A -> Type v) -> Type v

 def Verb (T : EventT {universe u}) : Type (lmax u (lsuc v))
   => Quantifier {universe u, v} (Event T)

-def mkVerb {T : EventT {universe u}} (p : Event {universe u} T -> Type (lmax u v))
+def mkVerb {T : EventT {universe u}} (p : Event {universe u} T -> Type)
-  : Verb {universe u, lmax u v} T
+  : Verb T
   => \f => Sig (e : Event {universe u} T) (s : p e) ** (f e)

Please note that all the code in this issue are different from each other plus the code in #11.

The code in #11 would also fail with explicit universe levels added in mkVerb. I don't know why.

[refparo]

I still believe the original code is right, resending here with as much universe information specified as possible:

universe u v

open data EventT : Type (lsuc u)
  | CarrierT (A : Type u)

def GetAgentT (T : EventT {universe u}) : Type u
  | CarrierT A => A

struct Event (T : EventT {universe u}) : Type u
  | agent : GetAgentT T

def Quantifier (A : Type u) : Type (lmax u (lsuc v)) => (A -> Type v) -> Type v

def Verb (T : EventT {universe u}) : Type (lmax u (lsuc v))
  => Quantifier (Event T {universe u}) {universe u, v}

def mkVerb {T : EventT {universe u}} (p : Event T {universe u} -> Type (lmax u v))
  : Verb T {universe u, lmax u v}
  -- = Quantifier (Event T {universe u}) {universe u, lmax u v}
  -- = ((Event T {universe u}) -> Type (lmax u v)) -> Type (lmax u v)
  => \(f : (Event T {universe u}) -> Type (lmax u v))
    => Sig (e : Event T {universe u}) (s : p e) ** (f e)
    -- Event T : Type u
    -- p e : Type (lmax u v)
    -- f e : Type (lmax u v)
    -- --------------------------------
    -- Sig (e : Event T) (p e) ** (f e)
    --   : Type (lmax u (lmax u v) (lmax u v)) = Type (lmax u v)

Please tell me if I got anything wrong.

[ice1000]

Universe polymorphism mechanism is completely replaced by McBride universes (https://mazzo.li/epilogue/index.html%3Fp=857&cpage=1.html).