compiler construction - implementar tipo de inferencia

compiler-construction functional-programming (5)

Veo algunas discusiones interesantes aquí sobre tipado estático vs. dinámico. Por lo general, prefiero el tipado estático, debido a la verificación del tipo de compilación, el código mejor documentado, etc. Sin embargo, estoy de acuerdo en que desordenan el código si se hace de la manera en que lo hace Java, por ejemplo.

Así que estoy a punto de comenzar a construir un lenguaje de estilo funcional propio, y la inferencia de tipo es una de las cosas que quiero implementar. Entiendo que es un gran tema, y no estoy tratando de crear algo que no se haya hecho antes, solo inferencia básica ...

¿Alguna sugerencia sobre qué leer que me ayude con esto? Preferiblemente, algo más pragmático / práctico en comparación con los textos de teorías de categorías / teorías de categorías más teóricas. Si hay un texto de discusión de implementación, con estructuras de datos / algoritmos, eso sería simplemente encantador.

Es lamentable que gran parte de la literatura sobre el tema sea muy densa. Yo también estaba en tus zapatos. Recibí mi primera introducción a la asignatura de Lenguajes de programación: aplicaciones e interpretación

http://www.plai.org/

Trataré de resumir la idea abstracta seguida de detalles que no encontré inmediatamente obvios. Primero, se puede pensar en la inferencia tipo generando y luego resolviendo restricciones. Para generar restricciones, recurse a través del árbol de sintaxis y genere una o más restricciones en cada nodo. Por ejemplo, si el nodo es un operador ''+'', los operandos y los resultados deben ser todos números. Un nodo que aplica una función tiene el mismo tipo que el resultado de la función, y así sucesivamente.

Para un lenguaje sin ''dejar'', puede resolver ciegamente las restricciones anteriores por sustitución. Por ejemplo:

(if (= 1 2) 1 2)

aquí, podemos decir que la condición de la sentencia if debe ser booleana, y que el tipo de la instrucción if es el mismo que el tipo de sus cláusulas "then" y "else". Como sabemos que 1 y 2 son números, por sustitución, sabemos que la declaración "si" es un número.

Donde las cosas se ponen desagradables, y lo que no pude entender por un tiempo, se trata de dejar:

(let ((id (lambda (x) x))) (id id))

Aquí, hemos vinculado ''id'' a una función que devuelve lo que haya pasado, también conocida como función de identidad. El problema es que el tipo del parámetro de la función ''x'' es diferente en cada uso de id. El segundo ''id'' es una función de a-> a, donde a puede ser cualquier cosa. El primero es de (a-> a) -> (a-> a) Esto se conoce como let-polymorphism. La clave es resolver las restricciones en un orden particular: primero resuelve las restricciones para la definición de ''id''. Esto será a-> a. Luego, las copias nuevas y separadas del tipo de identificación se pueden sustituir en las restricciones para cada lugar donde se usa ''id'', por ejemplo a2-> a2 y a3-> a3.

Eso no se explicó fácilmente en los recursos en línea. Mencionarán el algoritmo W o M pero no cómo funcionan en términos de resolución de restricciones, o por qué no descarta el polimorfismo let: cada uno de esos algoritmos impone un orden para resolver las restricciones.

Encontré este recurso extremadamente útil para unir el algoritmo W, M y el concepto general de generación de restricciones y resolver todos juntos. Es un poco denso, pero mejor que muchos:

http://www.cs.uu.nl/research/techreps/repo/CS-2002/2002-031.pdf

Muchos de los otros documentos que hay también son agradables:

http://people.cs.uu.nl/bastiaan/papers.html

Espero que eso ayude a aclarar un mundo algo turbio.

Lambda the Ultimate, comenzando aquí .

Tipos y Lenguajes de Programación por Benjamin C. Pierce

Los siguientes recursos me resultaron útiles para comprender la inferencia de tipos, en orden creciente de dificultad:

Capítulo 30 (Inferencia de tipo) del libro disponible gratuitamente PLAI , Lenguajes de programación: Aplicación e interpretación , bosquejo basado en la inferencia de tipo de unificación.
El curso de verano Interpretar tipos como valores abstractos presenta evaluadores elegantes, verificadores de tipos, reconstructors de tipo e inferencias usando Haskell como metalenguaje.
Capítulo 7 (Tipos) del libro EOPL , Essentials of Programming Languages .
Capítulo 22 (Reconstrucción de tipos) del libro TAPL , Tipos y lenguajes de programación , y las implementaciones OCaml correspondientes Recon y Fullrecon .
Capítulo 13 (Reconstrucción de tipos) del nuevo libro DCPL , Conceptos de diseño en lenguajes de programación .
Selección de trabajos académicos .
TypeInference del compilador de cierre es un ejemplo del enfoque de análisis de flujo de datos para la inferencia de tipo, que se adapta mejor a los lenguajes dinámicos que aborda Hindler Milner.

Sin embargo, dado que la mejor manera de aprender es hacerlo, sugiero implementar la inferencia de tipo para un lenguaje funcional de juguete trabajando en la asignación de tareas de un curso de lenguajes de programación.

Recomiendo estas dos tareas accesibles en ML, que pueden completarse en menos de un día:

PCF Interpreter ( una solución ) para calentar.
Inferencia de tipo PCF ( una solución ) para implementar el algoritmo W para la inferencia de tipo Hindley-Milner.

Estas asignaciones son de un curso más avanzado:

Además de Hindley Milner para los lenguajes funcionales, otro enfoque popular para la inferencia de tipo para el lenguaje dinámico es abstract interpretation .

La idea de la interpretación abstracta es escribir un intérprete especial para el idioma, en lugar de mantener un entorno de valores concretos (1, falso, cierre), funciona en valores abstractos, también conocidos como tipos (int, bool, etc.). Dado que está interpretando el programa en valores abstractos, es por eso que se llama interpretación abstracta.

Pysonar2 es una elegante implementación de interpretación abstracta para Python. Es utilizado por Google para analizar proyectos de Python. Básicamente, utiliza un visitor pattern para enviar una llamada de evaluación al nodo AST relevante. La transform función de visitante acepta el context en el que se evaluará el nodo actual y devuelve el tipo de nodo actual.