sobre - ¿Cómo completó Haskell la completitud de Turing con el Sistema F?

multiplos en haskell

Question

He estado leyendo sobre varios sistemas de tipos y cálculos lambda, y veo que todos los cálculos lambda tipados en el cubo lambda son fuertemente normalizadores en lugar de equivalentes de Turing. Esto incluye el Sistema F, el cálculo simplemente lambda más polimorfismo.

Esto me lleva a las siguientes preguntas, para las cuales no he podido encontrar ninguna respuesta comprensible:

• ¿Cómo se diferencia el formalismo de (por ejemplo) Haskell del cálculo en el que se basa ostensiblemente?
• ¿Qué características del lenguaje en Haskell no caen dentro del formalismo del Sistema F?
• ¿Cuál es el cambio mínimo necesario para permitir que Turing complete el cálculo?

Muchas gracias a quien me ayude a entender esto.

Answer 1

En una palabra, recursión general.

Haskell permite la recursión arbitraria mientras que el Sistema F no tiene forma de recursión. La falta de tipos infinitos significa que la fix no se puede expresar como un término cerrado.

No hay una noción primitiva de nombres y recursión. ¡De hecho, el Sistema F puro no tiene ninguna noción de definiciones!

Entonces, en Haskell esta única definición es lo que agrega una mayor integridad

fix :: (a -> a) -> a
fix f = let x = f x in x

Realmente esta función es indicativa de una idea más general, al tener enlaces completamente recursivos, obtenemos la integridad completa. Tenga en cuenta que esto se aplica a los tipos, no solo a los valores.

data Rec a = Rec {unrec :: Rec a -> a}

y :: (a -> a) -> a
y f = u (Rec u)
  where u x = f $ unrec x x

Con infinitos tipos, podemos escribir el combinador Y (módulo algo desplegado) y, a través de él, recursión general.

En el Sistema F puro, a menudo tenemos una noción informal de definiciones, pero estas son simplemente palabras cortas que deben ser mentalmente completadas. Esto no es posible en Haskell ya que esto crearía términos infinitos.

El núcleo de los términos de Haskell sin ninguna noción de let , where o = es fuertemente normalizador, ya que no tenemos infinitos tipos. Incluso este término central de cálculo no es realmente el Sistema F. El Sistema F tiene "grandes lambdas" o tipo de abstracción. El término completo para id en el Sistema F es

id := // A -> /(x : A) -> x

¡Esto se debe a que la inferencia de tipo para el Sistema F es indecidible! Registramos explícitamente dónde y cuándo esperamos el polimorfismo. En Haskell, tal propiedad sería molesta, por lo que limitamos el poder de Haskell. En particular, nunca inferimos un tipo polimórfico para un argumento de Haskell lambda sin anotación (pueden aplicarse términos y condiciones). Es por eso que en ML y Haskell

let x = exp in foo

no es lo mismo que

(/x -> foo) exp

incluso cuando exp no es recursivo! Este es el quid de la inferencia de tipo HM y el algoritmo W, llamado "let generalization".