the type of a pi type.

Stream: general

[Adam Kurkiewicz]

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?

[Simon Hudon]

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

[Kenny Lau]

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

[Simon Hudon]

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

[Simon Hudon]

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.

[Adam Kurkiewicz]

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.

[Simon Hudon]

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)

[Moses Schönfinkel]

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 :).

[Adam Kurkiewicz]

@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)

[Simon Hudon]

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

[Moses Schönfinkel]

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

[Simon Hudon]

@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

[Adam Kurkiewicz]

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.

[Simon Hudon]

Interesting detail:

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

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

[Moses Schönfinkel]

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

[Simon Hudon]

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

[Moses Schönfinkel]

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.

[Adam Kurkiewicz]

@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?

[Reid Barton]

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

[Moses Schönfinkel]

<deleted>

[Reid Barton]

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

[Adam Kurkiewicz]

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.

[Simon Hudon]

Do you mean that nat -> Prop example?