types - teoria - Estudio intenso de sistemas de tipos y teoría de tipos

teoria de los tipos quimica (1)

Quiero comprender la teoría real detrás de los tipos en lugar de simplemente aprender sobre el último cambio práctico realizado en algún lenguaje existente (por ejemplo, no solo cómo funciona el sistema de tipos de Haskell o Scala).

¿Cuál es la mejor manera de recoger este fondo?

La teoría de tipos es una gran área. En primer lugar, el término "tipos" es una especie de nombre inapropiado en ciencias de la computación, por algunas razones, a pesar de que se utilizan principalmente para la misma idea básica. Los tipos han surgido en muchos contextos, filosofía, ciencias de la computación y matemáticas, por la mayoría de las mismas razones. El origen de los tipos en las matemáticas proviene de tratar de formalizar la teoría de conjuntos y encontrarse con las paradojas esenciales, aunque surgen paradojas similares en la informática. (Por ejemplo, me gustaría señalar la paradoja de Girard en este caso).

La forma en que probablemente interpreta los tipos en el momento actual es una idea que se popularizó durante las décadas de 1970 y 1990 en computadoras: los tipos son un análisis liviano insensible al flujo que nos permite hacer garantías lógicas concisas sobre los programas que escribimos. Se pueden usar tipos para esto, pero en realidad puede llevarlos hasta la codificación de lógica de orden superior, donde los programas son pruebas . Una vez que vaya aquí, puede tomar una prueba, extraer el componente computacional y convertirlo en un programa que calcule un resultado "correcto" (con respecto al teorema que demostró).

Hay algunos caminos que puede tomar desde aquí:

Consígase una copia de los Tipos y Lenguajes de Programación de Ben Pierce . Este es el libro para leer, y uno de los mejores libros de ciencias de la computación. ¡Cubre la teoría de por qué necesitamos tipos y cómo podemos usarlos para imponer restricciones sobre nuestros programas!
Aprenda un idioma en el que utilice tipos de forma regular para aplicar cosas sobre la semántica del programa. En particular, puedes aprender OCaml, Haskell o Agda. Haskell parece ser la mejor opción en este momento, tiene bastantes extensiones que la hacen realmente atractiva y una comunidad de usuarios realmente activa. De hecho, es muy común que los resultados publicados en las principales conferencias fluyan a un uso generalizado en la comunidad en tan solo unos pocos años.
Aprende a usar un probador de teoremas basado en una teoría de tipos constructiva. En mi opinión, esta es la única forma real de asimilar los problemas reales detrás de la teoría de tipos. Hay una serie de buenas opciones, aunque Coq e Isabelle se destacan como los verdaderos contendientes ahora. Coq tiene una gran ventaja: ¡Ben Pierce también tiene un libro que lo cubre! Las Fundaciones de software cubren una cantidad de teoría de Lenguajes de programación en profundidad, y realmente puedes probar cosas que la usan.

Es posible que también desee examinar algunos campos relacionados:

La teoría de categorías es la matemática que tiende a subyacer a esto. Por ejemplo, es posible llevar una interpretación categórica a tipos de datos (co) inductivos dados en estos idiomas.
Lógica. Aprender un poco sobre la buena lógica tradicional puede ser útil, aunque confío en que la mayor parte de lo que necesita puede leerse en el libro de ciencia ficción de Ben Pierce. Sin embargo, todavía hay mucha referencia a los sistemas más antiguos (cálculo secuencial y deducción natural).
¡Aprende sobre la comunidad Haskell ! Se están moviendo rápidamente, como dije, y hacen preguntas profundas sobre los tipos en ciencias de la computación.
Great Works in Programming Languages tiene una serie de excelentes artículos.

Hay algunas recomendaciones excelentes que tengo para aprender más allá de esto, pero definitivamente comenzaría con los libros de Ben Pierce (nunca había entrado en el libro de seguimiento "temas avanzados en tipos y ciencias de la computación", pero eso también es quizás interesante). para ti). En particular, recuerdo que el Manual de razonamiento automatizado tiene un excelente artículo sobre la teoría de tipos de alto orden.

PD, estoy convencido de que la respuesta a esta pregunta es concretamente "obtener un doctorado en lenguajes de programación, filosofía o lógica ..." ;-)