He leído Introducción a la programación funcional mediante el cálculo lambda de Greg Michaelson, y me pareció un recurso muy bueno para aprender sobre el cálculo lambda no tipado. Sin embargo, también quiero aprender sobre las versiones tipadas del Cálculo Lambda, ya que a mi entender parecen ser la base de la mayoría de los lenguajes de programación funcional tipados estáticamente como Haskell. Desafortunadamente, todos los recursos que he encontrado en línea no explican la sintaxis de ninguna de las versiones tipadas del Cálculo Lambda muy bien, y no hace falta decir que esto hace que sea muy difícil de aprender. ¿Alguien sabe de algún buen recurso para aprender la versión simplemente tipada o cualquier otra versión tipada del Cálculo Lambda? Son preferibles los recursos gratuitos en línea, pero un libro de precio decente sobre el tema también estaría bien. Estoy buscando una introducción suave, no un libro de texto riguroso.
Respuestas
¿Demasiados anuncios?
Puedes probar Introducción al cálculo lambda de Barendregt y Barendsen, a partir del capítulo 5 ("Asignación de tipos"). El capítulo 5 sólo tiene 8 páginas, así que sabrá rápidamente si no es lo que está buscando $\ddot\smile$ .
Puede que esté desconcertado porque está buscando una sintaxis adicional para los tipos, pero no hay necesariamente ninguna sintaxis nueva. Los tipos pueden asignarse a los términos de forma implícita o explícita. El primer caso se llama "al estilo de Curry" y el segundo "al estilo de Church". En el estilo Curry del cálculo lambda tipado, la sintaxis es exactamente la misma que en el cálculo no tipado. La diferencia entre el cálculo tipado estilo Curry y el cálculo no tipado es que los términos tienen tipos asociados, no como parte de la sintaxis del lenguaje, sino implícitamente, y no se permite componer dos términos $S$ y $T$ a menos que los tipos coincidan correctamente.
Tipos y lenguajes de programación de Benjamin C. Pierce es el libro de texto estándar de introducción a este tema. No es barato y es riguroso, pero se puede leer con bastante facilidad sin preocuparse demasiado por el rigor, y es muy bueno.
Tengo formación en CS y me ha gustado mucho leer "Lambda-Calculus and Combinators: An Introduction" de Roger Hindley. Es un libro muy bueno para el autoaprendizaje porque tiene muchos ejercicios con soluciones. Después de leerlo pude hojear "An Introduction to Functional Programming Through Lambda Calculus" muy rápidamente, así que creo que este libro es bueno. Introduce el cálculo lambda no tipado así como dos tipos de cálculo lambda tipado. También describe la lógica combinatoria, que es aún más minimalista que el cálculo lambda.
