Simon está basicamente correto, do ponto de vista extensional. Sabemos muito bem o que são as semânticas das linguagens funcionais modernas, e elas realmente são variações relativamente pequenas uma da outra - cada uma representa traduções ligeiramente diferentes para uma metalinguagem monádica. Mesmo uma linguagem como Scheme (uma linguagem imperativa de ordem superior dinamicamente digitada e com controle de primeira classe) possui uma semântica bastante próxima da ML e Haskell.
V
Mas, para chegar a uma categoria adequada para interpretar linguagens funcionais digitadas modernas, as coisas ficam bastante assustadoras. Basicamente, você acaba construindo uma categoria enriquecida por ultrametria de relações de equivalência parcial sobre esse domínio. (Como exemplo, consulte "Semântica de realizabilidade do polimorfismo paramétrico, referências gerais e tipos recursivos de Birkedal, Stovring e Thamsborg".) As pessoas que preferem a semântica operacional conhecem esse material como relações lógicas indexadas por etapas. (Por exemplo, consulte "Independência da representação dependente do Estado" de Ahmed, Dreyer e Rossberg.) De qualquer maneira, as técnicas utilizadas são relativamente novas.
a -> b
⟨ Um ⟩ → T⟨ B ⟩⟨ Um ⟩ → ⟨ b ⟩T( A )⟨ Um ⟩a
→
No que diz respeito à teoria equacional, uma vez que essas línguas podem ser descritas por traduções em subconjuntos ligeiramente diferentes da mesma língua, é inteiramente justo chamá-las de variações sintáticas uma da outra.
A diferença de sensação entre ML e Haskell na verdade decorre das propriedades intensivas das duas linguagens - isto é, tempo de execução e consumo de memória. O ML possui um modelo de desempenho composicional (ou seja, o custo de tempo / espaço de um programa pode ser calculado a partir dos custos de tempo / espaço de seus subtermos), assim como seria uma verdadeira linguagem de chamada por nome. O Haskell real é implementado com chamada por necessidade, um tipo de memorização e, como resultado, seu desempenho não é composicional - o tempo que uma expressão vinculada a uma variável leva para avaliar depende se ela foi usada antes ou não. Isso não é modelado na semântica a que aludi acima.
Se você deseja levar as propriedades intensionais mais a sério, ML e Haskell começam a mostrar diferenças mais sérias. Provavelmente ainda é possível conceber uma metalinguagem comum para eles, mas a interpretação dos tipos diferirá de uma maneira muito mais sistemática, relacionada à idéia de focar na teoria da prova . Um bom lugar para aprender sobre isso é a tese de doutorado de Noam Zeilberger.