Simon es básicamente correcto, desde un punto de vista extensional. Sabemos bastante bien cuál es la semántica de los lenguajes funcionales modernos, y realmente son variaciones relativamente pequeñas entre sí: cada uno representa traducciones ligeramente diferentes en un metalenguaje monádico. Incluso un lenguaje como Scheme (un lenguaje imperativo de orden superior de tipo dinámico con control de primera clase) tiene una semántica muy parecida a la de ML y Haskell.
V
Pero para llegar a una categoría adecuada para interpretar lenguajes funcionales mecanografiados modernos, las cosas se ponen bastante aterradoras. Básicamente, terminas construyendo una categoría enriquecida ultramétrica de relaciones de equivalencia parcial sobre este dominio. (Como ejemplo, vea Birkedal, Stovring y Thamsborg, "Semántica de realizabilidad del polimorfismo paramétrico, referencias generales y tipos recursivos"). Las personas que prefieren la semántica operativa conocen estas cosas como relaciones lógicas indexadas por pasos. (Por ejemplo, ver "Independencia de representación dependiente del estado" de Ahmed, Dreyer y Rossberg). De cualquier manera, las técnicas utilizadas son relativamente nuevas.
a -> b⟨ Un ⟩ → T⟨ B ⟩⟨ Un ⟩ → ⟨ b ⟩T( A )⟨ Un ⟩a→
En lo que respecta a la teoría de la ecuación, dado que estos lenguajes pueden describirse mediante traducciones a subconjuntos ligeramente diferentes del mismo idioma, es completamente justo llamarlos variaciones sintácticas entre sí.
La diferencia de sensación entre ML y Haskell en realidad surge de las propiedades intensionales de los dos idiomas, es decir, el tiempo de ejecución y el consumo de memoria. ML tiene un modelo de rendimiento de composición (es decir, el costo de tiempo / espacio de un programa puede calcularse a partir de los costos de tiempo / espacio de sus subterms), como lo haría un verdadero lenguaje de llamada por nombre. Haskell real se implementa con una llamada por necesidad, una especie de memorización, y como resultado, su rendimiento no es compositivo: el tiempo que tarda una expresión vinculada a una variable en evaluar depende de si se ha utilizado antes o no. Esto no está modelado en la semántica a la que aludí anteriormente.
Si desea tomar las propiedades intensivas más en serio, ML y Haskell comienzan a mostrar diferencias más serias. Todavía es posible idear un metalenguaje común para ellos, pero la interpretación de los tipos diferirá de una manera mucho más sistemática, relacionada con la idea teórica de la prueba de enfoque . Un buen lugar para aprender sobre esto es la tesis doctoral de Noam Zeilberger.
