Zulip Chat Archive

Stream: general

Topic: the type of a pi type.


view this post on Zulip Adam Kurkiewicz (Mar 15 2018 at 19:08):

After a few months break I am revisiting lean basics. I'm looking back at dependent types.

I understand why this typechecks: ((λ k: nat, eq.refl k) : (Π k : nat, k = k)) essentially we have a function, which returns a type, which depends on the parameter the function takes. We need this because we want to have a family of proofs 0 = 0, 1 = 1, etc.

But I don't get why these typecheck: ((Π k : nat, k = k) : Prop) or ((Π k: nat, Prop) : Type). The rule seems to be that the type signature of any pi type "forgets" the parameters that the type on the left depends on and behaves as if it was a simple type.

Are there any particular reasons of why that is or is it just the way it is?

view this post on Zulip Simon Hudon (Mar 15 2018 at 19:13):

Yes. Let's look at the non-dependent case first. Let's first notice that everything has a type:

(λ n : ℕ, n+1) : ℕ → ℕ
ℕ → ℕ : Type 0
Type 0 : Type 1
-- and so on

view this post on Zulip Kenny Lau (Mar 15 2018 at 19:13):

@Adam Kurkiewicz if A has type u and B has type v, then A -> B has type max u v

view this post on Zulip Simon Hudon (Mar 15 2018 at 19:15):

And ℕ → ℕ is basically syntactic sugar for Π n : ℕ, ℕ

view this post on Zulip Simon Hudon (Mar 15 2018 at 19:24):

The rule seems to be that the type signature of any pi type "forgets" the parameters that the type on the left depends on and behaves as if it was a simple type.

That's correct.

Are there any particular reasons of why that is or is it just the way it is?

For one thing it is useful. But let's look at an alternative:

(Π k : nat, k = k) : nat -> Prop

That means that that proposition is not true on its own. It would be true about a given number. But that's not the case. Π is the same as . The statement is not "if you give me a number, I'll state that it is equal to itself". It is "every number is equal to itself". If you want the first, you'll use (λ k : nat, k = k) : nat -> Prop. It is not an assertion on its own. You feed it a natural number and then the result will state something about that natural number.

view this post on Zulip Adam Kurkiewicz (Mar 15 2018 at 19:27):

I see. So it doesn't forget the type of the parameter, it just takes the maximum of the type of the parameter and the type of the type. So Prop is effectively Type -1, right? And since nat : Type 0, then k : Type -1 and k = k : Type -1 is Type -1, so the total result is Type max -1 -1, which is Type -1, which is Prop. This might be a little bit barbarian, but I think I'm getting it.

view this post on Zulip Simon Hudon (Mar 15 2018 at 19:29):

A less barbarian way of seeing is that Prop and Type are both syntactic sugar for Sort: Prop = Sort 0 and Type u = Sort (u+1)

view this post on Zulip Moses Schönfinkel (Mar 15 2018 at 19:30):

I am surprised you would care so much about universes (given that you are a beginner I assume). This information is not very useful in my opinion :).

view this post on Zulip Adam Kurkiewicz (Mar 15 2018 at 19:31):

@Simon Hudon I actually do not think that my original statement was correct. The type of the parameter is not forgotten, it's the maximum like @Kenny Lau said, for example this typechecks #check ((Π k: Type 0, Prop) : Type 1)

view this post on Zulip Simon Hudon (Mar 15 2018 at 19:31):

Really? For small proofs maybe but as soon as you have types within types, you have to start caring about universes

view this post on Zulip Moses Schönfinkel (Mar 15 2018 at 19:32):

Not quite. You can rely on Type* to do the work for you.

view this post on Zulip Simon Hudon (Mar 15 2018 at 19:34):

@Simon Hudon I actually do not think that my original statement was correct. The type of the parameter is not forgotten, it's the maximum like @Kenny Lau said, for example this typechecks #check ((Π k: Type 0, Prop) : Type 1)

That's true, in that sense, it does not forget. More specifically, it does not forget the universe of the parameter. The type itself becomes unavailable though

view this post on Zulip Adam Kurkiewicz (Mar 15 2018 at 19:35):

I've largely ignored universes so far, and most of the underlying type theory, but given that I might be teaching lean to others from next semester I'm trying to make sure I know at least a little bit of the foundations.

view this post on Zulip Simon Hudon (Mar 15 2018 at 19:35):

Interesting detail:

#check ((Π k: Type 7, k = k) : Prop)

If the result type is Prop, the whole thing can stay in Prop

view this post on Zulip Moses Schönfinkel (Mar 15 2018 at 19:35):

I think you've done well to ignore them for the most part :P!

view this post on Zulip Simon Hudon (Mar 15 2018 at 19:36):

I think I agree. I don't particularly like to have to specify them. I wonder what justify that design choice

view this post on Zulip Moses Schönfinkel (Mar 15 2018 at 19:38):

I use Type* and only think about it once I run into issues. From my experience, I find it not too difficult to fix them post-facto. I have yet to encounter a case where I wish I had considered it beforehand. But perhaps I avoid the kinds of things that might require more universe-thought. I mostly write certificates of functional programs.

view this post on Zulip Adam Kurkiewicz (Mar 15 2018 at 19:40):

@Simon Hudon hmm... So it turns out it's not max u vafter all? It can't be, since in this case it would have to be Type 7 as opposed to Prop?

view this post on Zulip Reid Barton (Mar 15 2018 at 19:42):

It's actually imax u v which is 0 if v is 0, and otherwise max u v.

view this post on Zulip Moses Schönfinkel (Mar 15 2018 at 19:42):

<deleted>

view this post on Zulip Reid Barton (Mar 15 2018 at 19:43):

Useful to know mainly because you might see imax in Lean output/error messages and wonder what it means, I think.

view this post on Zulip Adam Kurkiewicz (Mar 15 2018 at 19:48):

Thanks @Reid Barton, this will definitely come useful at some point.

@Simon Hudon I really like your example with natural numbers. I think it's another productive way of thinking about Pi types.

view this post on Zulip Simon Hudon (Mar 15 2018 at 19:49):

Do you mean that nat -> Prop example?


Last updated: May 10 2021 at 19:16 UTC