Zulip Chat Archive

Stream: new members

Topic: prod and pprod


Horatiu Cheval (Apr 11 2021 at 05:45):

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 (Apr 11 2021 at 05:51):

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 (Apr 11 2021 at 05:53):

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 (Apr 11 2021 at 05:54):

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

Horatiu Cheval (Apr 11 2021 at 06:09):

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 1\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 (Apr 11 2021 at 06:11):

Or is this not the way things work?

Mario Carneiro (Apr 11 2021 at 06:15):

The problem is that -1 isn't a thing

Mario Carneiro (Apr 11 2021 at 06:15):

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

Mario Carneiro (Apr 11 2021 at 06:16):

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

Horatiu Cheval (Apr 11 2021 at 06:19):

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 (Apr 11 2021 at 06:22):

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 (Apr 11 2021 at 06:23):

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 (Apr 11 2021 at 06:25):

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 (Apr 11 2021 at 06:25):

right

Mario Carneiro (Apr 11 2021 at 06:25):

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

Mario Carneiro (Apr 11 2021 at 06:26):

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

Mario Carneiro (Apr 11 2021 at 06:27):

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

Mario Carneiro (Apr 11 2021 at 06:30):

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 (Apr 11 2021 at 06:31):

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

Horatiu Cheval (Apr 11 2021 at 06:33):

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


Last updated: Dec 20 2023 at 11:08 UTC