haskell - "¿Qué parte de Hindley-Milner no entiendes?"

functional-programming lambda-calculus (6)

Juro que solía haber una camiseta en venta con las palabras inmortales:

Que parte de

no entiendes

En mi caso, la respuesta sería ... ¡todo!

En particular, a menudo veo una notación como esta en los documentos de Haskell, pero no tengo ni idea de lo que significa. No tengo idea de qué rama de las matemáticas se supone que debe ser.

Reconozco las letras del alfabeto griego, por supuesto, y símbolos como "∉" (que generalmente significa que algo no es un elemento de un conjunto).

Por otro lado, nunca he visto "⊢" antes ( Wikipedia dice que podría significar "partición" ). Tampoco estoy familiarizado con el uso del vinculum aquí. (Por lo general, denota una fracción, pero ese no parece ser el caso aquí).

Si alguien al menos pudiera decirme dónde empezar a buscar para comprender qué significa este mar de símbolos, eso sería útil.

si alguien al menos pudiera decirme dónde empezar a buscar para comprender qué significa este mar de símbolos

Consulte " Fundamentos prácticos de los lenguajes de programación ", capítulos 2 y 3, sobre el estilo de la lógica a través de juicios y derivaciones. El libro completo ya está disponible en Amazon.

Capitulo 2

Definiciones Inductivas

Las definiciones inductivas son una herramienta indispensable en el estudio de los lenguajes de programación. En este capítulo desarrollaremos el marco básico de definiciones inductivas y daremos algunos ejemplos de su uso. Una definición inductiva consiste en un conjunto de reglas para derivar juicios , o aseveraciones , de una variedad de formas. Los juicios son declaraciones sobre uno o más objetos sintácticos de un tipo específico. Las reglas especifican condiciones necesarias y suficientes para la validez de un juicio y, por lo tanto, determinan completamente su significado.

2.1 juicios

Comenzamos con la noción de un juicio o afirmación sobre un objeto sintáctico. Haremos uso de muchas formas de juicio, incluyendo ejemplos como estos:

n nat - n es un número natural
n = n1 + n2 - n es la suma de n1 y n2
τ tipo - τ es un tipo
e : τ - la expresión e tiene el tipo τ
e ⇓ v - expresión e tiene valor v

Un juicio establece que uno o más objetos sintácticos tienen una propiedad o se relacionan entre sí. La propiedad o relación en sí se llama forma de juicio , y el juicio de que un objeto u objetos tienen esa propiedad o posición en esa relación se dice que es una instancia de esa forma de juicio. Una forma de juicio también se denomina predicado , y los objetos que constituyen una instancia son sus sujetos . Escribimos una J para el juicio afirmando que J sostiene de a . Cuando no es importante enfatizar el tema del juicio, (el texto se corta aquí)

¿Cómo entiendo las reglas de Hindley-Milner?

Hindley-Milner es un conjunto de reglas en forma de cálculo secuencial (no de deducción natural) que dice que puede deducir el tipo (más general) de un programa a partir de la construcción del programa sin declaraciones explícitas de tipo.

Los símbolos y la notación.

Primero, vamos a explicar los símbolos.

𝑥 es un identificador (informalmente, un nombre de variable).
: significa es un tipo de (informalmente, una instancia de, o "is-a").
𝜎 (sigma) es una expresión que es una variable o una función.
∈ significa es un elemento de
𝚪 (Gamma) es un entorno.
⊦ (el signo de aserción) significa afirmaciones (o pruebas, pero contextualmente "afirma" se lee mejor).
𝚪⊦ 𝑥 : 𝜎 se lee así 𝚪 afirma 𝑥, a 𝜎
𝑒 es una instancia real (elemento) de tipo 𝜎 .
𝜏 (tau) es un tipo: ya sea básico, variable ( 𝛼 ), funcional 𝜏 → 𝜏 '' o producto 𝜏 × 𝜏''
𝜏 → 𝜏 '' es un tipo funcional donde 𝜏 y 𝜏'' son tipos.
𝜆𝑥.𝑒 significa que 𝜆 (lambda) es una función anónima que toma un argumento, 𝑥 , y devuelve una expresión, 𝑒 .
sea 𝑥 = 𝑒₀ en 𝑒₁ significa en expresión, 𝑒₁ , sustituye 𝑒₀ donde aparezca 𝑥 .
⊑ significa que el elemento anterior es un subtipo (informalmente - subclase) del último elemento.
𝛼 es una variable de tipo.
∀ 𝛼.𝜎 es un tipo, ∀ (para todas) las variables de argumento, 𝛼 , que devuelve 𝜎 expresión
∉ libre (𝚪) significa que no es un elemento de las variables de tipo libre de 𝚪 definidas en el contexto externo. (Las variables unidas son sustituibles.)

Todo lo que está por encima de la línea es la premisa, todo lo que está abajo es la conclusión ( Per Martin-Löf )

Lo que sigue a continuación son interpretaciones en inglés de las declaraciones lógicas, seguidas de una explicación.

Variable

Dado que 𝑥 es un tipo de 𝜎 (sigma), un elemento de 𝚪 (Gamma),
Concluir 𝚪 afirma 𝑥 es un 𝜎.

Esto es básicamente una tautología, un nombre de identificador es una variable o una función.

Aplicación de la función

Dado que 𝚪 afirma 𝑒₀ es un tipo funcional y 𝚪 afirma 𝑒₁ es un
Concluir 𝚪 afirma que aplicar la función 𝑒₀ a 𝑒₁ es un tipo 𝜏 ''

Esto significa que si sabemos que una función devuelve un tipo y lo aplicamos a un argumento, el resultado será una instancia del tipo que sabemos que devuelve.

Función de abstracción

Dado que 𝜏 y 𝑥 de tipo 𝜏 aseveraciones 𝑒 es un tipo, 𝜏 ''
Concluir 𝚪 afirma una función anónima, 𝜆 de 𝑥 devolver la expresión, 𝑒 es de tipo 𝜏 → 𝜏 ''.

Esto significa que si sabemos que 𝑥 es de tipo 𝜏 y, por lo tanto, una expresión 𝑒 es de tipo 𝜏 '', entonces una función de 𝑥 que devuelve expresión 𝑒 es de tipo 𝜏 → 𝜏''.

Dejar declaración de variable

Dado que 𝚪 afirma 𝑒₀, de tipo 𝜎, y 𝚪 y 𝑥, de tipo 𝜎, afirma 𝑒₁ de tipo 𝜏
concluya 𝚪 afirma let let = 𝑒₀ in 𝑒₁ de tipo 𝜏

Esto significa que si tenemos una expresión 𝑒₀ que es un 𝜎 (que es una variable o una función), y algún nombre, 𝑥, también un 𝜎, y una expresión 𝑒₁ de tipo 𝜏, entonces podemos sustituir 𝑒₀ por donde aparezca. de 𝑒₁.

Instanciación

Dado que 𝚪 afirma 𝑒 de tipo 𝜎 ''y 𝜎'' es un subtipo de 𝜎
concluye 𝚪 afirma 𝑒 es de tipo 𝜎

Esto significa que si una instancia es de un tipo que es un subtipo de otro tipo, también es una instancia de ese supertipo.

Esto nos permite utilizar la creación de instancias de tipo en el sentido más general de que una expresión puede devolver un tipo más específico.

Generalización

Dado que 𝚪 afirma 𝑒 es un 𝜎 y 𝛼 no es un elemento de las variables libres de 𝚪,
concluya 𝚪 afirma 𝑒, escriba para todas las expresiones de argumento 𝛼 devolviendo una 𝜎 expresión

Esto significa que podemos generalizar un programa para que acepte todos los tipos de argumentos que aún no están vinculados en el ámbito de contenido (variables que no son no locales). Estas variables unidas son sustituibles.

Conclusión

Estas reglas combinadas nos permiten probar el tipo más general de un programa afirmado, sin requerir anotaciones de tipo, permitiendo que varios tipos sean aceptados correctamente como entrada (polimorfismo paramétrico).

Esta sintaxis, aunque puede parecer complicada, es bastante simple. La idea básica proviene de la lógica: toda la expresión es una implicación, siendo la mitad superior las suposiciones y la mitad inferior el resultado. Es decir, si sabe que las expresiones superiores son verdaderas, puede concluir que las expresiones inferiores también son verdaderas.

Simbolos

Otra cosa a tener en cuenta es que algunas letras tienen significados tradicionales; en particular, Γ representa el "contexto" en el que se encuentra, es decir, cuáles son los tipos de otras cosas que ha visto. Entonces, algo como Γ ⊢ ... significa "la expresión ... cuando conoces los tipos de cada expresión en Γ .

El símbolo ⊢ significa esencialmente que puedes probar algo. Entonces Γ ⊢ ... es una declaración que dice "puedo probar ... en un contexto Γ . Estas declaraciones también se denominan juicios de tipo.

Otra cosa a tener en cuenta: en matemáticas, al igual que ML y Scala, x : σ significa que x tiene el tipo σ . Puedes leerlo igual que Haskell''s x :: σ .

Lo que significa cada regla

Entonces, sabiendo esto, la primera expresión se vuelve fácil de entender: si sabemos que x : σ ∈ Γ (es decir, x tiene algún tipo σ en algún contexto Γ ), entonces sabemos que Γ ⊢ x : σ (es decir, en Γ , x tiene el tipo σ ). Así que realmente, esto no te dice nada super interesante; simplemente te dice cómo usar tu contexto.

Las otras reglas también son simples. Por ejemplo, tomar [App] . Esta regla tiene dos condiciones: e₀ es una función de algún tipo τ a algún tipo τ'' y e₁ es un valor de tipo τ . ¡Ahora sabe qué tipo obtendrá al aplicar e₀ a e₁ ! Esperemos que esto no sea una sorpresa :).

La siguiente regla tiene una sintaxis más nueva. En particular, Γ, x : τ solo significa el contexto formado por Γ y el juicio x : τ . Entonces, si sabemos que la variable x tiene un tipo de τ y la expresión e tiene un tipo τ'' , también conocemos el tipo de una función que toma x y devuelve e . Esto solo nos dice qué hacer si hemos averiguado qué tipo toma una función y qué tipo devuelve, por lo que tampoco debería ser sorprendente.

El siguiente solo te dice cómo manejar las declaraciones de let . Si sabe que alguna expresión e₁ tiene un tipo τ siempre que x tenga un tipo σ , entonces una expresión let que localmente se enlaza con x a un valor de tipo σ hará que e₁ tenga un tipo τ . En realidad, esto solo le dice que una declaración de dejar esencialmente le permite expandir el contexto con un nuevo enlace, ¡que es exactamente lo let deja!

La regla [Inst] se ocupa de la subtitulación. Dice que si tiene un valor de tipo σ'' y es un subtipo de σ ( ⊑ representa una relación de orden parcial), entonces esa expresión también es de tipo σ .

La regla final trata de generalizar tipos. Un lado rápido: una variable libre es una variable que no es introducida por una declaración let o lambda dentro de alguna expresión; esta expresión ahora depende del valor de la variable libre de su contexto. La regla dice que si hay alguna variable α que no es "libre" en nada en su contexto, entonces es seguro decir que cualquier expresión cuyo tipo sea know e : σ tendrá ese tipo para cualquier valor de α .

Como usar las reglas.

Entonces, ahora que entiendes los símbolos, ¿qué haces con estas reglas? Bueno, puedes usar estas reglas para averiguar el tipo de varios valores. Para hacer esto, mire su expresión (diga fxy ) y busque una regla que tenga una conclusión (la parte inferior) que coincida con su declaración. Llamemos a lo que estás tratando de encontrar tu "objetivo". En este caso, vería la regla que termina en e₀ e₁ . Cuando haya encontrado esto, ahora tiene que encontrar reglas que prueben todo por encima de la línea de esta regla. Estas cosas generalmente corresponden a los tipos de subexpresiones, por lo que esencialmente se está repitiendo en partes de la expresión. Solo haz esto hasta que termines tu árbol de pruebas, lo que te da una prueba del tipo de expresión.

Por lo tanto, todas estas reglas sí es especificar exactamente, y en el detalle matemático habitual: P, cómo averiguar los tipos de expresiones.

Ahora, esto debería sonar familiar si alguna vez ha usado Prolog; básicamente está calculando el árbol de pruebas como un intérprete humano de Prolog. ¡Hay una razón por la que Prolog se llama "programación lógica"! Esto también es importante ya que la primera forma en que me introdujeron en el algoritmo de inferencia HM fue implementándolo en Prolog. Esto es en realidad sorprendentemente simple y deja claro lo que está pasando. Sin duda debes intentarlo.

Nota: Probablemente cometí algunos errores en esta explicación y me encantaría que alguien los señalara. De hecho, estaré cubriendo esto en clase en un par de semanas, así que estaré más seguro entonces: P.

Hay dos maneras de pensar en e: σ. Una es "la expresión e tiene el tipo σ", otra es "el par ordenado de la expresión e y el tipo σ".

Ver Γ como el conocimiento sobre los tipos de expresiones, implementado como un conjunto de pares de expresiones y tipos, e: σ.

El torniquete ⊢ significa que a partir del conocimiento de la izquierda, podemos deducir lo que hay a la derecha.

La primera regla [Var] se puede leer así:
Si nuestro conocimiento Γ contiene el par e: σ, entonces podemos deducir de Γ que e tiene el tipo σ.

La segunda regla [App] se puede leer:
Si desde podemos deducir que e_0 tiene el tipo τ → τ '', y desde Γ podemos deducir que e_1 tiene el tipo τ, entonces desde Γ podemos deducir que e_0 e_1 tiene el tipo τ''.

Es común escribir Γ, e: σ en lugar de Γ ∪ {e: σ}.

La tercera regla [Abs] se puede leer así:
Si desde Γ extendido con x: τ podemos deducir que e tiene el tipo τ '', entonces desde Γ podemos deducir que λx.e tiene el tipo τ → τ''.

La cuarta regla [Let] se deja como ejercicio. :-)

La quinta regla [Inst] se puede leer:
Si desde podemos deducir que e tiene el tipo σ '', y σ'' es un subtipo de σ, entonces desde Γ podemos deducir que e tiene el tipo σ.

La sexta y última regla [Gen] se puede leer:
Si desde Γ podemos deducir que e tiene el tipo σ, y α no es una variable de tipo libre en ninguno de los tipos en Γ, entonces desde Γ podemos deducir que e tiene el tipo α σ.

La notación proviene de la deducción natural .

⊢ símbolo se llama turnstile .

Las 6 reglas son muy fáciles.

Var regla Var es una regla bastante trivial: dice que si el tipo de identificador ya está presente en su entorno de tipo, para inferir el tipo, simplemente lo toma del entorno tal como está.

App regla de la App dice que si tiene dos identificadores e0 y e1 y puede inferir sus tipos, entonces puede inferir el tipo de aplicación e0 e1 . La regla dice así si sabes que e0 :: t0 -> t1 y e1 :: t0 (¡el mismo t0!), Entonces la aplicación está bien escrita y el tipo es t1 .

Abs y Let son reglas para inferir tipos para lambda-abstraction y let-in.

Inst regla de Inst dice que puedes sustituir un tipo por uno menos general.

La barra horizontal significa que "[arriba] implica [abajo]".
Si hay varias expresiones en [arriba], entonces considérelas y juntas; todos los [arriba] deben ser verdaderos para garantizar el [abajo].
: significa tiene tipo
∈ significa que está en . (Del mismo modo, ∉ significa "no está en".)
Γ se utiliza generalmente para referirse a un entorno o contexto; en este caso, se puede considerar como un conjunto de anotaciones de tipo, emparejando un identificador con su tipo. Por lo tanto, x : σ ∈ Γ significa que el entorno Γ incluye el hecho de que x tiene el tipo σ .
⊢ se puede leer como prueba o determina. Γ ⊢ x : σ significa que el entorno Γ determina que x tiene el tipo σ .
, es una forma de incluir suposiciones adicionales específicas en un entorno.
Por lo tanto, Γ, x : τ ⊢ e : τ'' significa que el entorno Γ , con la suposición adicional y adicional de que x tiene el tipo τ , demuestra que e tiene el tipo τ'' .

Según lo solicitado: precedencia del operador, de mayor a menor:

Operadores de infijo y mixfix específicos del idioma, como λ x . e λ x . e , ∀ α . σ ∀ α . σ , y τ → τ'' , let x = e0 in e1 , y espacios en blanco para la aplicación de función.
:
∈ y ∉
, (asociativo a la izquierda)
⊢
espacios en blanco separando proposiciones multiples (asociativas)
la barra horizontal