haskell - programacion - ¿Milner deja que el polimorfismo sea un rasgo de rango 2?

polimorfismo java

Question

let a = b in c se pueda pensar como un azúcar sintáctico para (/a -> c) b , pero en una configuración escrita en general no es el caso. Por ejemplo, en el cálculo de Milner let a = /x -> x in (a True, a 1) se puede escribir let a = /x -> x in (a True, a 1) , pero aparentemente equivalente (/a -> (a True, a 1)) (/x -> x) es no.

Sin embargo, este último es tipificable en el Sistema F con un tipo de rango 2 para la primera lambda.

Mis preguntas son:

• ¿Es el polimorfismo una característica de rango 2 que se ocultó secretamente en el mundo de lo contrario rango 1 del cálculo de Milner?

• El propósito de tener una construcción separada de let parece especificar qué tipos deben generalizarse por el comprobador de tipos y cuáles no. ¿Tiene algún otro propósito? ¿Hay alguna razón para extender sistemas más poderosos, por ejemplo, el Sistema F con una separación separada que no es azúcar? ¿Hay algún artículo sobre el fundamento del diseño del cálculo de Milner que ya no me parece obvio?

• ¿Existe el tipo más general para /a -> (a True, a 1) en el Sistema F?

• ¿Hay sistemas de tipo cerrado bajo expansión beta? Es decir, si P es tipificable y MN = P, entonces M tipificable?

Algunas aclaraciones:

• Por equivalencia me refiero a las anotaciones de tipo de módulo de equivalencia. ¿Es ''System F a la Church'' el término correcto para eso?

• Sé que, en general, la propiedad de escritura principal no se mantiene en F, pero podría existir un tipo principal para mi término particular.

• Al decir me refiero al sabor no recursivo de let . La extensión del sistema F con un permiso recursivo es obviamente útil ya que permite la no terminación.

Answer 1

Los tipos no se conservan bajo expansión beta en ningún cálculo que pueda expresar el concepto de "código muerto". Probablemente puedas descubrir cómo escribir algo similar a esto en cualquier lenguaje utilizable:

if True then something typable else utter nonsense

Por ejemplo, vamos a M = (/xy -> x) (something typable) y N = (utter nonsense) y P = (something typable) , de modo que MN = P , y P se puede escribir, pero MN no.

... releyendo tu pregunta, veo que solo exiges que M sea ​​tipificable, pero me parece un significado muy extraño para "preservado bajo expansión beta" para mí. De todos modos, no veo por qué algún argumento como el anterior no podría aplicarse: simplemente deje que M tenga un código muerto que no se puede escribir en él.

Answer 2

No puedo responder a todas sus preguntas muy especializadas, pero no, no es una función de rango 2. Mientras escribe, es solo que las definiciones se cuantifiquen, lo que produce un tipo de rango 1 totalmente polimórfico, a menos que la definición dependa de algún valor monomórfico en un ámbito nouterino.

Tenga en cuenta que Haskell let se conoce como let rec en otros idiomas y permite la definición de funciones y valores recursivos entre sí. Esto es algo que no querría codificar manualmente con expresiones lambda y combinadores en Y.

Answer 3

Para las cuatro preguntas formuladas:

• Una idea clave en este asunto es que, en lugar de simplemente escribir una abstracción lambda con un tipo de argumento potencialmente polimórfico, estamos escribiendo una abstracción (azucarada) que se aplica (1) exactamente una vez y, además, se aplica (2) Un argumento estáticamente conocido. Es decir, primero podemos someter el "argumento" (es decir, los definiens de la definición local) al tipo de reconstrucción para encontrar su tipo (polimórfico); luego asigne el tipo encontrado al "parámetro" (el definiendum); y luego, finalmente, escriba el cuerpo en el contexto de tipo extendido.

  Tenga en cuenta que eso es considerablemente más fácil que la inferencia general de tipo rango 2.

• Tenga en cuenta que, hablando estrictamente, deje que ... = .. en ... sea solo azúcar sintáctica en el Sistema F si exige que el definiendum incluya una anotación de tipo: deje que:: = = .. en ...

• Aquí hay dos soluciones para T en (/ a :: T -> (a True, a 1)) en el Sistema F: para todos b. (para todos a. a -> b) -> (b, b) y para todos c d. (para todos a b. a -> b) -> (c, d). Tenga en cuenta que ninguno de ellos es más general que el otro. En general, el Sistema F no admite tipos principales.

• Supongo que esto vale para el cálculo lambda simplemente escrito?

Answer 4

Puede escribir (/a -> (a True, a 1)) (/x -> x) si en lugar de generalizar solo expresiones, generalice todas las abstracciones lambda. Una vez hecho esto, también es necesario crear una instancia de los esquemas de tipo en cada punto de uso, no simplemente en el punto donde realmente se utiliza la carpeta que se refiere a ellos. No creo que haya ningún problema con esto en realidad, aparte del hecho de que es mucho menos eficiente. Recuerdo una discusión de esto en TAPL, de hecho, haciendo puntos similares.

Answer 5

Recuerdo que hace muchos años vi en un libro sobre cálculo lambda (posiblemente Barendregt) un sistema de tipos conservado por la expansión beta. No tenía cuantificación, pero tenía disyunción para expresar que un término debía ser de más de un tipo simultáneamente, así como un tipo especial omega que habitaba cada término. Como recuerdo, este último evita la objeción del código muerto de Daniel Wagner. Si bien cada expresión estaba bien escrita, restringir la posición de omega en el tipo le permitía caracterizar qué expresiones tenían (¿débiles?) Las formas normales de la cabeza.

Además, si recuerdo correctamente, las expresiones de formas completamente normales tenían tipos principales, que no contenían omega.

Por ejemplo, el tipo principal de / fx -> f (fx) (el número 2 de la Iglesia) sería algo como ((A -> B) / / (B -> C)) -> A -> C