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
λ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
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?
Oh, silly of me,
λ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 -> t because this makes two alpha-equivalent terms
\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
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.