¿Por qué necesitamos una notación separada para los tipos P?

Question

Principal

Estoy confundido acerca de la motivación detrás de la necesidad de una notación separada para los tipos П, que se pueden encontrar en los sistemas de tipos desde λ2 en adelante.La respuesta suele ser la siguiente: piense en cómo se puede representar una firma de función de identidad: puede ser λa:type.λx:a.x o λb:type.λx:b.x.La parte sutil, dicen, es que estas dos firmas no sólo not equal, no son equivalentes alfa como variables de tipo a y b son variables libres dentro de sus correspondientes abstracciones.Entonces, para superar este molesto problema sintáctico, presentamos la carpeta P que funciona muy bien con la conversión alfa.

Entonces la pregunta:¿porqué es eso?¿Por qué no simplemente corregir la noción de equivalencia alfa?

ACTUALIZACIÓN z:

Oh, tonto de mi parte, λa:type.λx:a.x y λb:type.λx:b.x son equivalentes alfa.Pero por qué a:type -> a -> a y b:type -> b -> b Entonces no lo son.

ACTUALIZAR como z:

Ajá, interesante, supongo que este es un ejemplo perfecto de ceguera selectiva =D

Estoy leyendo el libro Teoría de tipos y prueba formal, y en el capítulo sobre lambda2 el autor motiva la existencia de П usando exactamente ese tipo de argumentación; no se puede decir que \t:*.\v:t.v : * -> t -> t porque esto hace dos términos equivalentes alfa\t:*.\v:t.v y \g:*.\v:g.v tienen diferentes tipos, ya que los tipos correspondientes no son equivalentes alfa, donde tipos como t:* -> t -> t de hecho son alfa-invariantes. Cuidado con la diferencia entre t:* -> t -> t y * -> t -> t.Pero, ¿no hace que este argumento sea un poco trivial, y es incluso algo significativo hablar sobre el tipo? a -> b dónde a y b no están vinculados por ninguna variable cuantificadora.Andrej Bauer señaló en los comentarios que П De hecho, esto se parece a una abstracción lambda con algunas campanas y silbidos adicionales.

Considerándolo todo, ya terminé con eso, gracias chicos..

Answer 1

Creo que sólo necesitamos aclarar algunas cosas aquí:

1. en la expresión $\lambda a :\mathsf{tipo}.\lambda x :a .x$ La variable $a$ esta obligado (por el exterior $\lambda$).Las expresiones $\lambda a :\mathsf{tipo}.\lambda x :a .x$ y $\lambda b :\mathsf{tipo}.\lambda x :b .x$ son $\alfa$-igual.
2. La expresion $\lambda a :\mathsf{tipo}.\lambda x :a .x$ es la función de identidad, es no la "firma de la función de identidad".
3. Si por "firma de la función de identidad" quiere decir "el tipo de función de identidad", entonces sería algo como $\Pi_{a :\mathsf{tipo}} .(a \a a)$, o si solo desea tipos de productos, entonces es $\Pi_{a :\mathsf{tipo}} \Pi_{x :a} a$.

¿Todavía hay una pregunta?

Tal vez esto ayude:

• el tipo de función de identidad $\lambda x :a .x$ es $a \a $
• el tipo de función de identidad $\lambda y :b .y$ es $b \a b$
• Las funciones $\lambda x :a .x$ y $\lambda y :b .y$ son diferentes
• los tipos $a \a $ y $b \a b$ son diferentes
• el tipo de polimórfico función de identidad $\lambda c :\mathsf{tipo}.\lambda z :C .z$ es $\Pi_{c :\mathsf{tipo}} .c \a c$.
• Las funciones $\lambda a :\mathsf{tipo}.\lambda x :a .x$ y $\lambda c :\mathsf{tipo}.\lambda z :C .z$ son $\alfa$-igual
• los tipos $\Pi_{a :\mathsf{tipo}} .un \a un $ y $\Pi_{c :\mathsf{tipo}} .c \a c$ son $\alfa$-igual.

Hecho suplementario: Después de hablar con Alex Simpson mientras tomamos una taza de té, hay una cosa más que puedo decir.nosotros no necesidad separado $\lambda$ y $\Pi$ constructores, ya que ambos tienen exactamente la misma forma sintáctica (tomar dos argumentos, vincular una variable).De hecho, si mi memoria no me falla, autómata usó la misma notación para $\lambda$-abstracciones y $\Pi$-tipos.Pero el punto es que nosotros desear utilizar dos constructores diferentes porque denotan diferentes conceptos.