Why do we need a separate notation for П-types?

Question

Main

I am confused about the motivation behind the need for a separate notation for П-types, that you can find in type systems from λ2 on. The answer usually goes like so - think about how one can represent a signature of identity function - it can be λa:type.λx:a.x or λb:type.λx:b.x. The subtle part, they say, is that these two signatures not only not equal, they are not alpha-equivalent as type variables a and b are free variables inside their correspondent abstractions. So to overcome this pesky syntactic issue, we present П binder that plays nicely with alpha-conversion.

So the question: why is that? Why not just fix the notion of alpha-equivalence?

UPDATE z:

Oh, silly of me, λa:type.λx:a.x and λb:type.λx:b.x are alpha equivalent. But why a:type -> a -> a and b:type -> b -> b arent then.

UPDATE suc z:

Aha, interesting, I guess this is a perfect example of selective blindness =D

I am reading the book Type Theory and Formal Proof, and in the chapter about lambda2 author motivates the existence of П using exactly that kind of argumentation - one cant say that \t:*.\v:t.v : * -> t -> t because this makes two alpha-equivalent terms\t:*.\v:t.v and \g:*.\v:g.v have different types, as corresponding types are not alpha-equivalent, where types like t:* -> t -> t are in fact alpha-invariant. Mind the difference between t:* -> t -> t and * -> t -> t. But, doesn't it make this argument a bit trivial, and is it even something meaningful to talk about type a -> b where a and b are unbound by any quantifiers variables. Andrej Bauer pointed out in the comments that П is indeed resembles a lambda abstraction with a few additional bells and whistles.

All in all, I am done with that one, thank you guys.

Answer 1

I think we just need to get some things straight here:

1. In the expression $\lambda a : \mathsf{type} . \lambda x : a . x$ the variable $a$ is bound (by the outer $\lambda$). The expressions $\lambda a : \mathsf{type} . \lambda x : a . x$ and $\lambda b : \mathsf{type} . \lambda x : b . x$ are $\alpha$-equal.
2. The expression $\lambda a : \mathsf{type} . \lambda x : a . x$ is the identity function, it is not the "signature of the identity function".
3. If by "signature of the identity function" you mean to say "the type of the identity function", then it would be something like $\Pi_{a : \mathsf{type}} . (a \to a)$, or if you want only product types, then it is $\Pi_{a : \mathsf{type}} \Pi_{x : a} a$.

Is there still a question?

Maybe this will help:

• the type of the identity function $\lambda x : a . x$ is $a \to a$
• the type of the identity function $\lambda y : b . y$ is $b \to b$
• the functions $\lambda x : a . x$ and $\lambda y : b . y$ are different
• the types $a \to a$ and $b \to b$ are different
• the type of the polymorphic identity function $\lambda c : \mathsf{type} . \lambda z : c . z$ is $\Pi_{c : \mathsf{type}} . c \to c$.
• the functions $\lambda a : \mathsf{type} . \lambda x : a . x$ and $\lambda c : \mathsf{type} . \lambda z : c . z$ are $\alpha$-equal
• the types $\Pi_{a : \mathsf{type}} . a \to a$ and $\Pi_{c : \mathsf{type}} . c \to c$ are $\alpha$-equal.

Supplemental: After talking to Alex Simpson over a cup of tea, there is one more thing I can say. We don't need separate $\lambda$ and $\Pi$ constructors, as they both have precisely the same syntactic shape (take two arguments, bind one variable). In fact, if my memory serves me right, Automath used the same notation for $\lambda$-abstractions and $\Pi$-types. But the point is that we want to use two different constructors because they denote different concepts.