Zulip Chat Archive

Stream: new members

Topic: prod and pprod


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 11 2021 at 05:54):

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

view this post on Zulip 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)?

view this post on Zulip Horatiu Cheval (Apr 11 2021 at 06:11):

Or is this not the way things work?

view this post on Zulip Mario Carneiro (Apr 11 2021 at 06:15):

The problem is that -1 isn't a thing

view this post on Zulip Mario Carneiro (Apr 11 2021 at 06:15):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 11 2021 at 06:25):

right

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Horatiu Cheval (Apr 11 2021 at 06:31):

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

view this post on Zulip 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: May 13 2021 at 05:21 UTC