Empecé a leer más y más trabajos de investigación lingüística. Me parece muy interesante y una buena manera de aprender más sobre la programación en general. Sin embargo, generalmente viene una sección en la que siempre lucho (tome, por ejemplo, la tercera parte de esto ) ya que no tengo los antecedentes teóricos en informática: Reglas de tipo.
¿Hay buenos libros o recursos en línea disponibles para comenzar en esta área? Wikipedia es increíblemente vaga y realmente no ayuda a un principiante.
Respuestas:
En la mayoría de los sistemas de tipos, las reglas de tipos trabajan juntas para definir juicios de la forma:
Esto establece que en el contexto la expresión e tiene el tipo τ . Γ es un mapeo de las variables libres de e a sus tipos.Γ e τ
Γ e
Un sistema de tipos consistirá en un conjunto de axiomas y reglas (un sistema formal de reglas de inferencia , como señala Rafael).
Un axioma es de la forma
Esto establece que el juicio es válido (siempre).Γ⊢e:τ
Un ejemplo es
que establece que bajo el supuesto de que el tipo de variable es τ , entonces la expresión x tiene el tipo τ .x τ x τ
Las reglas de inferencia toman hechos que ya han sido determinados y construyen hechos más grandes a partir de ellos. Por ejemplo, la regla de inferencia
dice que si tengo una derivación del hecho y una derivación del hecho Γ ⊢ e 2 : τ , entonces puedo obtener una derivación del hecho Γ ⊢ e 1 e 2 : τ ′ . En este caso, esta es la regla para escribir la aplicación de función.Γ⊢e1:τ→τ′ Γ⊢e2:τ Γ⊢e1 e2:τ′
Hay dos formas de leer esta regla:
Algunas reglas de inferencia también manipulan al agregarle nuevos ingredientes (ver de abajo hacia arriba). Aquí está la regla para la abstracción λ :Γ λ
Las reglas de inferencia se aplican inductivamente en función de la sintaxis de la expresión que se considera que forma un árbol de derivación. En las hojas del árbol (en la parte superior) habrá axiomas, y las ramas se formarán aplicando reglas de inferencia. En la parte inferior del árbol está la expresión que le interesa escribir.
Por ejemplo, una derivación de la tipificación de la expresión esλf.λx.f x
Dos libros muy buenos para aprender sobre sistemas de tipos son:
Ambos libros son muy completos, pero comienzan lentamente, construyendo una base sólida.
fuente
Hay un lindo tutorial interactivo en línea sobre cálculo secuencial, que puede ayudar a construir algunas intuiciones y sentir cómo funciona la inferencia: un tutorial interactivo del cálculo secuencial
fuente
En esa página de Wikipedia se recomienda " Type Systems, Luca Cardelli, ACM Computing Surveys ", que es una encuesta de 2 páginas que puede ayudarlo a comprender cómo leer una regla. De todos modos, cómo leer una regla se explica perfectamente en esa página de Wikipedia (o incluso mejor en la encuesta de 2 páginas). Sin embargo, para comprenderlo todo, debe comprender qué es un sistema de mecanografía (compuesto por varias reglas), para el cual el artículo de Wikipedia " Sistema de texto " es un buen comienzo (y tiene varios libros en la sección " Referencias " de ese página si quieres ir más allá).
fuente