prod and pprod

Stream: new members

[Horatiu Cheval]

What's the reason, or the use-case of having distinct Type-valued and general Sort-valued analogous definitions like prod/pprod and the like? I don't understand why one doesn't have just the more general pprod and uses that in all situations, even when only Types are involved; it seems like in principle you could do that. So, what's the reason for this design? Thanks in advance!

[Mario Carneiro]

pprod is a straight generalization of prod, so it can be used anywhere prod is, in principle. But the target universe of pprod is Sort (max 1 u v) which can be difficult to unify with other things

[Mario Carneiro]

In particular, there is no solution to the equation Sort (max 1 u v) = Type ?, so an arbitrary pprod will not be accepted where a Type ? is required

[Mario Carneiro]

example {α β} := set (α × β) -- ok
example {α β} := set (pprod α β) -- fail

[Horatiu Cheval]

I don't know much about how unification works, so I'm just speaking intuitively and I'm probably wrong, but since max 1 u v is $\ge 1$, isn't it always a Type, namely Type (max 1 u v) - 1, so to say? Isn't Type u just a notation for Sort (u + 1)?

[Horatiu Cheval]

Or is this not the way things work?

[Mario Carneiro]

The problem is that -1 isn't a thing

[Mario Carneiro]

the syntax of levels contains 0, _ + 1, max _ _, imax _ _ and variables

[Mario Carneiro]

In that language, there is no term representing max 1 u v - 1, even though that is a natural number

[Horatiu Cheval]

I knew I couldn't write -1 there in Lean, but I thought that maybe internally, in the implementation Lean could do other natural number manipulations besides what I'm allowed to write in universe arguments. But I get it now, thanks!

[Mario Carneiro]

The unification algorithm, when faced with the goal max 1 u v = ? + 1, has to find an actual term for ? making the two sides equal, and there is no such term (there is if you substitute u+1 for u and v+1 for v, though)

[Mario Carneiro]

that impoverished grammar is actually baked into the kernel (and external typecheckers), so the elaborator isn't allowed to do magic with it

[Horatiu Cheval]

So universes are represented in the kernel as actual terms in the language you described, not as some generic natural number datatype, right?

[Mario Carneiro]

right

[Mario Carneiro]

They can't be generic natural numbers anyway, because they have variables in them, u and v

[Mario Carneiro]

In fact, if these were numbers there would be no problem: max 1 0 4 = ? + 1 has a solution

[Mario Carneiro]

They can't be arbitrary terms of type nat either, because that would be inconsistent (which is a fun paradox)

[Mario Carneiro]

The paradox, by the way, involves the question of what universe λ n, Type n lives in; it's not hard to go from that to girard's paradox

[Horatiu Cheval]

Indeed, thank you, I think all is clear now with regards to unification

[Horatiu Cheval]

The paradox does seem interesting, I'll try to see how to get to Girard's paradox from there