3
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ They are $\alpha$-equivalent. $\endgroup$ – Andrej Bauer Aug 24 at 11:41
  • 2
    $\begingroup$ Still, $a : \mathsf{type} \to a \to a$ and $b : \mathsf{type} \to b \to b$ are $\alpha$-equivalent. That's just a variant notation for $\Pi$-types. Perhaps you need an updated update :-) $\endgroup$ – Andrej Bauer Aug 24 at 13:59
  • 1
    $\begingroup$ I hope this process will halt eventually. Please help, I am scared. $\endgroup$ – hello world Aug 24 at 15:04
  • 1
    $\begingroup$ It makes sense to speak of a -> b where a and b are free parameters (that's the positive way of saying "unbounded by any quantifier"). You can think of them as meta-variables, or schematic variables. It's exactly the same as the usual free and bound variables, but "one level up" at the level of types. $\endgroup$ – Andrej Bauer Aug 25 at 10:32
6
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ About point two - sorry about that, I do understand the difference, swear of that =D $\endgroup$ – hello world Aug 24 at 11:37
  • $\begingroup$ But what is your question? $\endgroup$ – Andrej Bauer Aug 24 at 11:40
  • $\begingroup$ The real reason of my confusion there is that I've always thought of a function type (a -> b) as being a syntax sugar on top of simple lambda abstraction. Say, f: int -> string only means f: (λa:type. λb:type. map(a, b))(int, string) to me, where map is really just a pair constructor. The Abs portion of the type has no free vars and thus can be renamed as I like, raising the queston, why do I need П. $\endgroup$ – hello world Aug 24 at 12:11
  • $\begingroup$ Is it true, that in a nutshell this П thing is somewhat equivalent to the map type constructor from the comment above? $\endgroup$ – hello world Aug 24 at 12:21
  • 1
    $\begingroup$ I made one more remark, perhaps it helps. $\endgroup$ – Andrej Bauer Aug 24 at 13:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.