Pregunta sobre el "Tutorial de la aplicación de dependencia escribió cálculo lambda"

Question

Tengo una ligera técnica de lucha con este maravilloso tutorial.En la página 5 el tutorial habla de escribir las reglas para el tipo simple de Lambdas y presenta la siguiente sentencia, como se desprende a través de reglas en la figura 3.

Yo era incapaz de probar ni id ni const por la misma razón.Tomemos por ejemplo el id ejemplo.

• Decir que estoy buscando en la comprobación del tipo de regla CHK.Se dice que en el fin de check types Primero debe realizar la inferencia y, a continuación, comparar el resultado con lo que se espera.
• Para hacer la inferencia sobre la aplicación, tengo que usar el APP la regla que de inmediato me obliga a inferir el tipo de la parte izquierda de la aplicación, es decir, (id :: α -> α)
• Para hacer que estoy utilizando el ANN la regla que me obliga a comprobar que α -> α es un tipo (y puedo probarlo no hay problema).Entonces tengo esta desnudo id símbolo y tiene que probar que es un tipo de ser α -> α.
• Finalmente, aquí hay un problema.Con el fin de hacer que voy a tener que usar var la regla, que requiere el tipo de id en el contexto de la Gamma de forma explícita, pero esto no se hace, por lo tanto la prueba está cayendo a pedazos.

Answer 1

$\mathsf{id}$ y $\mathsf{const}$ no son variables de la ecuación, pero azúcar sintáctico para $\lambda x ightarrow x$ y $\lambda x ightarrow \lambda y ightarrow x$ respectivamente.Esto se afirma al final del §2.2 y sutilmente se transmite mediante el uso de una fuente sans-serif lugar de itálica (esta es una convención tipográfica de este documento particular, no una convención común).

Así por ejemplo, el tipo de juicio $$ \alpha ::\ast, y ::\alpha \vdash (\mathsf{id} ::\alpha ightarrow \alpha) \:y :: ightarrow \alpha $$ también es el tipo de juicio $$ \alpha ::\ast, y ::\alpha \vdash (\lambda x ightarrow x ::\alpha ightarrow \alpha) \:y :: ightarrow \alpha .$$ Es una notación diferente para el mismo objeto matemático.