Yo juro que solía ser una camiseta a la venta con las palabras inmortales:

Que parte de

es lo que no entiende?

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

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

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

Por otro lado, nunca había visto "⊢" antes ( Wikipedia afirma 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 por dónde empezar a buscar para comprender lo que significa este mar de símbolos, sería útil.

• La barra horizontal significa que "[arriba] implica [abajo]".
• Si hay varias expresiones en [arriba], considérelas juntas; todo lo anterior debe ser verdadero para garantizar lo siguiente.
• :significa tiene tipo
• ∈los medios están adentro . (Del mismo modo ∉significa "no está en").
• Γse usa generalmente para referirse a un entorno o contexto; en este caso, puede considerarse como un conjunto de anotaciones de tipo, que combina un identificador con su tipo. Por x : σ ∈ Γlo tanto, significa que el entorno Γincluye el hecho de que xtiene tipo σ.
• ⊢se puede leer como prueba o determina. Γ ⊢ x : σsignifica que el entorno Γdetermina que xtiene tipo σ.
• ,es una forma de incluir suposiciones adicionales específicas en un entorno Γ.
  Por lo tanto, Γ, x : τ ⊢ e : τ'significa que el entorno Γ, con el supuesto adicional de anulación que xtiene tipoτ , prueba que etiene tipo τ'.

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

• Infijos y mixfix operadores específicos del idioma, como por ejemplo λ x . e, ∀ α . σy τ → τ', let x = e0 in e1y un espacio en blanco para la aplicación de la función.
• :
• ∈ y ∉
• , (asociativo a la izquierda)
• ⊢
• espacios en blanco que separan múltiples proposiciones (asociativo)
• la barra horizontal

Esta sintaxis, si bien puede parecer complicada, en realidad es bastante simple. La idea básica proviene de la lógica formal: toda la expresión es una implicación, siendo la mitad superior los supuestos 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.

Los símbolos

Otra cosa a tener en cuenta es que algunas letras tienen significados tradicionales; particularmente, Γ 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 esencialmente significa que puedes probar algo. Entonces, Γ ⊢ ...hay una declaración que dice "Puedo probar ...en un contexto Γ. Estas declaraciones también se llaman juicios de tipo.

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

Qué significa cada regla

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

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

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

El siguiente solo te dice cómo manejar las letdeclaraciones. Si sabe que alguna expresión e₁tiene un tipo τsiempre que xtenga un tipo σ, entonces una letexpresión que se une localmente xa un valor de tipo σhará que e₁tenga un tipo τ. Realmente, esto simplemente le dice que una declaración let esencialmente le permite expandir el contexto con un nuevo enlace, ¡que es exactamente lo que lethace!

La [Inst]regla trata del subtipado. 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 los tipos de generalización. Un comentario 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 conozca e : σtendrá ese tipo para cualquier valor de α.

Cómo usar las reglas

Entonces, ahora que comprende los símbolos, ¿qué hace con estas reglas? Bueno, puedes usar estas reglas para descubrir el tipo de varios valores. Para hacer esto, mire su expresión (digamos f x y) y encuentre una regla que tenga una conclusión (la parte inferior) que coincida con su declaración. Llamemos a lo que está tratando de encontrar su "objetivo". En este caso, mirarías 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 estás recurriendo en partes de la expresión. Simplemente haga esto hasta que termine su árbol de pruebas, que le da una prueba del tipo de su expresión.

Entonces, todas estas reglas hacen especificar exactamente, y en el detalle matemáticamente pedante 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 Prolog humano. ¡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 presentaron el algoritmo de inferencia HM fue implementarlo en Prolog. En realidad, esto es sorprendentemente simple y deja en claro lo que está sucediendo. Ciertamente deberías probarlo.

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 tendré más confianza entonces: P.

si alguien al menos pudiera decirme dónde comenzar a buscar para comprender lo que 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. Todo el libro ya está disponible en Amazon.

Capitulo 2

Definiciones Inductivas

Las definiciones inductivas son una herramienta indispensable en el estudio de 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 aserciones , 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 las 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, incluidos ejemplos como estos:

• n nat - n es un número natural
• n = n1 + n2 - n es la suma de n1 y n2
• τ type - τ es un tipo
• e : τ - la expresión e tiene el tipo τ
• e ⇓ v - la 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 se mantienen en esa relación se dice que es una instancia de esa forma de juicio. Una forma de juicio también se llama predicado , y los objetos que constituyen una instancia son sus sujetos . Escribimos una J para el juicio afirmando que J tiene 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 deducción natural) que demuestra que podemos deducir el tipo (más general) de un programa a partir de la construcción del programa sin declaraciones de tipo explícitas.

Los símbolos y la notación.

Primero, expliquemos los símbolos y analicemos la precedencia del operador

• 𝑥 es un identificador (informalmente, un nombre de variable).
• : significa es un tipo de (informalmente, una instancia de, o "es-a").
• 𝜎 (sigma) es una expresión que es una variable o una función.
• así 𝑥: 𝜎 se lee " 𝑥 es-a 𝜎 "
• ∈ significa "es un elemento de"
• 𝚪 (Gamma) es un entorno.
• ⊦ (el signo de aserción) significa afirma (o prueba, pero contextualmente "afirma" se lee mejor).
• 𝚪 ⊦ 𝑥 : 𝜎 se lee así "𝚪 afirma que 𝑥, es-a 𝜎 "
• 𝑒 es una instancia real (elemento) de tipo 𝜎 .
• 𝜏 (tau) es un tipo: básico, variable ( 𝛼 ), funcional 𝜏 → 𝜏 ' o producto 𝜏 × 𝜏' (el producto no se usa aquí)
• 𝜏 → 𝜏 ' es un tipo funcional donde 𝜏 y 𝜏' son tipos potencialmente diferentes.

• 𝜆𝑥.𝑒 significa que 𝜆 (lambda) es una función anónima que toma un argumento, 𝑥 , y devuelve una expresión, 𝑒 .

• dejar 𝑥 = 𝑒₀ en 𝑒₁ significa en expresión, 𝑒₁ , sustituir 𝑒₀ 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) variables de argumento, 𝛼 , que devuelve la expresión 𝜎
• ∉ libre (𝚪) significa que no es un elemento de las variables de tipo libre de 𝚪 definidas en el contexto externo. (Las variables enlazadas son sustituibles).

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

Precedencia, por ejemplo

Tomé algunos de los ejemplos más complejos de las reglas e inserté paréntesis redundantes que muestran precedencia:

• 𝑥: 𝜎 ∈ 𝚪 podría escribirse (𝑥: 𝜎) ∈ 𝚪

• 𝚪 ⊦ 𝑥 : 𝜎 podría escribirse 𝚪 ⊦ ( 𝑥 : 𝜎 )

• 𝚪 ⊦ let 𝑥 = 𝑒₀ en 𝑒₁ : 𝜏 es equivalente 𝚪 ⊦ (( let ( 𝑥 = 𝑒₀ ) en 𝑒₁ ): 𝜏 )

• 𝚪 ⊦ 𝜆𝑥.𝑒 : 𝜏 → 𝜏 ' es equivalentemente 𝚪 ⊦ (( 𝜆𝑥.𝑒 ): ( 𝜏 → 𝜏' ))

Luego, los espacios grandes que separan las afirmaciones de afirmación y otras condiciones previas indican un conjunto de tales condiciones previas, y finalmente la línea horizontal que separa la premisa de la conclusión trae el final del orden de precedencia.

Las normas

Lo que sigue aquí son interpretaciones en inglés de las reglas, cada una seguida de una nueva declaración y una explicación.

Variable

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

Dicho de otra manera, en 𝚪, sabemos que 𝑥 es de tipo 𝜎 porque 𝑥 es de tipo 𝜎 en 𝚪.

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

Aplicación de funciones

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

Para reformular la regla, sabemos que la aplicación de función devuelve el tipo 𝜏 'porque la función tiene el tipo 𝜏 → 𝜏' y obtiene un argumento de tipo 𝜏.

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

Abstracción de funciones

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

Nuevamente, cuando vemos una función que toma 𝑥 y devuelve una expresión 𝑒, sabemos que es de tipo 𝜏 → 𝜏 'porque 𝑥 (a 𝜏) afirma que 𝑒 es a 𝜏'.

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

Dejar declaración variable

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

En términos generales, 𝑥 está vinculado a 𝑒₀ en 𝑒₁ (a 𝜏) porque 𝑒₀ es un 𝜎, y 𝑥 es un 𝜎 que afirma que 𝑒₁ es un 𝜏.

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 sea que aparezca dentro de 𝑒₁.

Instanciación

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

Una expresión, 𝑒 es de tipo padre 𝜎 porque la expresión 𝑒 es subtipo 𝜎 ', y 𝜎 es el tipo padre de 𝜎'.

Si una instancia es de un tipo que es un subtipo de otro tipo, entonces también es una instancia de ese supertipo, el tipo más general.

Generalización

Dado que rts 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 𝜎

Entonces, en general, 𝑒 se escribe 𝜎 para todas las variables de argumento (𝛼) que devuelven 𝜎, porque sabemos que 𝑒 es un a y 𝛼 no es una variable libre.

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

Poniendolo todo junto

Dados ciertos supuestos (como no hay variables libres / indefinidas, un entorno conocido), conocemos los tipos de:

• elementos atómicos de nuestros programas (Variable),
• valores devueltos por funciones (aplicación de función),
• construcciones funcionales (abstracción de funciones),
• enlaces de let (Declaraciones de variables de Let),
• tipos primarios de instancias (instanciación) y
• todas las expresiones (generalización).

Conclusión

Estas reglas combinadas nos permiten probar el tipo más general de un programa afirmado, sin requerir anotaciones de tipo.

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

El símbolo ⊢ se llama torniquete .

Las 6 reglas son muy fáciles.

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

AppLa regla dice que si tiene dos identificadores e0y e1puede inferir sus tipos, puede inferir el tipo de aplicación e0 e1. La regla se lee así si lo sabe e0 :: t0 -> t1y e1 :: t0(¡el mismo t0!), Entonces la aplicación está bien escrita y el tipo es t1.

Absy Letson reglas para inferir tipos para lambda-abstraction y let-in.

Inst La regla dice que puede sustituir un tipo con uno menos general.

Hay dos formas de pensar en e: σ. Uno es "la expresión e tiene tipo σ", otro 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 expresión y tipo, e: σ.

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

La primera regla [Var] puede leerse 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 escriba τ '.

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

La tercera regla [Abs] puede leerse 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] puede leerse:
si desde Γ podemos deducir que e tiene tipo σ, y α no es una variable de tipo libre en ninguno de los tipos en Γ, entonces desde Γ podemos deducir que e tiene tipo ∀α σ.