¿Cómo se debe leer la notación de los sistemas de tipos?

 (langdev.stackexchange.com)
1 puntos por GN⁺ 2023-08-17 | 1 comentarios | Compartir por WhatsApp
  • Aunque la notación de los sistemas de tipos varía según el material, si se entiende el marco común de gramática, relaciones de tipado y reglas de inferencia, se puede seguir la mayoría de las variantes
  • Un sistema de tipos opera sobre la sintaxis abstracta de un lenguaje, por lo que primero hay que distinguir gramaticalmente entre los términos (terms) que tienen tipo y los tipos en sí
  • ⊢ e: τ es un juicio de tipado que significa “la expresión e tiene el tipo τ”, y se lee como una regla de inferencia donde, si todas las condiciones sobre la línea horizontal son verdaderas, la conclusión debajo también lo es
  • Cuando aparecen variables y funciones, se agrega un contexto, como en Γ ⊢ e: τ, para rastrear los nombres de variables y sus tipos en el scope actual
  • Muchas reglas de tipado pueden leerse como una función recursiva de comprobación de tipos, pero no todo juicio lógico se convierte directamente en un algoritmo de comprobación de tipos decidible

Notación de sistemas de tipos a partir de la gramática

  • Un sistema de tipos es un sistema sintáctico de un lenguaje de programación y consiste en un conjunto de reglas que operan sobre la sintaxis abstracta del lenguaje
  • Una explicación completa de un sistema de tipos normalmente presenta primero las estructuras sintácticas que trata mediante una gramática, y las expresa con notación BNF
  • Incluso en el lenguaje tipado más simple, la sintaxis se divide a grandes rasgos en dos categorías
    • e: expresiones (expressions) que tienen tipo
    • τ: tipos (types) que se asignan a las expresiones
  • El lenguaje de ejemplo tiene como expresiones literales booleanos, literales enteros, expresiones condicionales, operaciones aritméticas y operaciones de comparación, y usa Bool e Int como tipos
  • Según el material, el símbolo de tipo puede escribirse como t, T, σ u otras letras griegas minúsculas en lugar de τ, pero la estructura general es similar
  • Los lenguajes más complejos pueden incluir más categorías sintácticas, como sentencias o patrones de pattern matching

Leer relaciones y juicios de tipado

  • Después de fijar la gramática, normalmente se define una relación de tipado de la forma e : τ
    • 1 + 2 : Int significa “1 + 2 es de tipo Int”
    • 1 + 2 : Bool significa que la misma expresión es de tipo Bool, por lo que no es correcto
    • true + 2 : Int no tiene sentido como expresión, así que no tiene ningún tipo
  • ⊢ e : τ es un juicio de tipado, y ⊢ puede leerse como “la afirmación que sigue es verdadera”
  • Una regla sin nada sobre la línea horizontal es un axioma (axiom), siempre verdadero
    • ⊢ true : Bool
    • ⊢ false : Bool
    • Reglas para literales enteros como ⊢ 0 : Int, ⊢ 1 : Int, ⊢ -1 : Int
  • Una regla con contenido tanto arriba como abajo de la línea horizontal es una regla de inferencia
    • Si todas las condiciones superiores son verdaderas, la conclusión inferior es verdadera
    • Si e₁ y e₂ son ambos Int, entonces e₁ + e₂ es Int
    • Si e₁ y e₂ son ambos Int, entonces e₁ < e₂ es Bool

Expresiones condicionales y variables de tipo

  • Las dos ramas de if ... then ... else ... pueden ser de cualquier tipo, pero deben tener el mismo tipo entre sí
    • if true then 1 else 2 es válido
    • if true then false else true es válido
    • if true then 1 else true no es válido
  • Para expresar esto, la regla usa la variable τ para representar el tipo de las ramas
    • La expresión condicional e₁ debe ser Bool
    • La rama then e₂ y la rama else e₃ deben tener el mismo tipo τ
    • El tipo de toda la expresión condicional también pasa a ser τ
  • Al aplicar la regla, se puede elegir cualquier tipo como τ, pero dentro de la misma regla esa elección debe mantenerse de forma consistente

Leer las reglas de inferencia como algoritmos

  • Esta notación proviene de la lógica formal, y la forma de especificar sistemas de tipos se parece especialmente a la deducción natural
  • Estas reglas se usan para construir pruebas formales sobre propiedades del sistema, y son importantes para demostrar propiedades como la seguridad de tipos
  • Un juicio lógico no siempre corresponde directamente a un algoritmo de comprobación de tipos decidible
  • En muchos casos, ⊢ e : τ puede leerse como una función que obtiene el tipo τ a partir de la expresión e
    • Para cada forma de expresión de la gramática normalmente hay una regla
    • Cada regla de tipado puede verse como una rama de una función recursiva de comprobación de tipos
  • La función infer del ejemplo corresponde al siguiente flujo
    • true o false es Bool
    • Un literal entero es Int
    • e₁ + e₂, después de comprobar que los resultados de inferir ambos lados son Int, es Int
    • e₁ < e₂, después de comprobar que ambos lados son Int, es Bool
    • if e₁ then e₂ else e₃ comprueba que la condición sea Bool, comprueba que los tipos de las dos ramas sean iguales y luego devuelve ese tipo
  • Aunque no pueda trasladarse directamente a un algoritmo, si se piensa en e como entrada y en τ como salida dentro del juicio, el flujo de información resulta más fácil de entender

Variables y contexto

  • Para tratar un lenguaje de programación útil se necesitan variables, y el ejemplo se amplía agregando funciones hasta tomar la forma del cálculo lambda simplemente tipado
  • La gramática extendida incluye lo siguiente
    • Variable x
    • Abstracción de función λx:τ. e
    • Aplicación de función e e
    • Tipo de función τ → τ
  • λx:τ. e corresponde a (x:τ) => e en TypeScript, y f x corresponde a f(x)
  • El tipo de una variable depende del contexto en el que aparece, así que no se puede escribir una regla con una forma simple como ⊢ x : ???
  • Por eso el juicio de tipado se extiende a Γ ⊢ e : τ
    • Γ es el contexto o entorno de tipos
    • ⊢ separa las suposiciones del contexto a la izquierda de la afirmación que se probará a la derecha
    • Se lee como “bajo el contexto Γ, la expresión e tiene el tipo τ”
  • Algorítmicamente, Γ puede verse como una entrada adicional con forma Map<Variable, Type>
  • Formalmente, el contexto también se especifica como una estructura sintáctica
    • ∅: contexto vacío
    • Γ, x:τ: contexto con un binding de variable agregado
    • A veces se usa • como contexto vacío en lugar de ∅
  • En esta representación, el contexto se parece a una lista de asociaciones que mapea nombres de variables a tipos

Qué hace el contexto dentro de las reglas

  • Muchas reglas de tipado pasan el contexto sin modificarlo
    • Γ ⊢ true : Bool
    • Si Γ ⊢ e₁ : Int y Γ ⊢ e₂ : Int, entonces Γ ⊢ e₁ + e₂ : Int
  • En las reglas de uso de variables y expresiones lambda, el contexto cumple un papel central
    • Si x:τ ∈ Γ, entonces Γ ⊢ x : τ
    • Si Γ, x:τ₁ ⊢ e : τ₂, entonces Γ ⊢ (λx:τ₁. e) : τ₁ → τ₂
  • Al comprobar el tipo del cuerpo e de una expresión lambda, el contexto se extiende con el nuevo binding x:τ₁
  • La regla de variables juzga que, si existe un binding de la variable en el contexto actual, esa variable tiene ese tipo
  • El contexto se usa como un mecanismo de comunicación que transmite información entre la regla de expresiones lambda y la regla de variables
  • Para simplificar, las especificaciones de sistemas de tipos de este estilo suelen asumir que todas las variables ya fueron resueltas y hechas únicas, y no tratan el shadowing de variables
  • La regla de aplicación de funciones comprueba conjuntamente los tipos de la expresión función y de la expresión argumento
    • e₁ debe tener el tipo τ₁ → τ₂
    • e₂ debe tener el tipo τ₁
    • El tipo de la aplicación completa e₁ e₂ pasa a ser τ₂

Notación adicional frecuente

  • Las reglas de inferencia no siempre se escriben solo en vertical
    • Varias condiciones pueden colocarse horizontalmente, una junto a otra
    • La disposición vertical y la horizontal pueden mezclarse dentro de la misma regla
  • Las condiciones sobre la línea horizontal normalmente son otros juicios, pero también pueden aparecer condiciones laterales (side conditions), es decir, condiciones booleanas arbitrarias
    • x:τ ∈ Γ en la regla de variables es un ejemplo
    • En sistemas de tipos algorítmicos puede usarse α fresh, lo que significa que α debe ser una variable de tipo nueva, distinta de las demás variables de tipo

Subtipado

  • El subtipado es una relación que trata la compatibilidad entre tipos de forma más flexible que la igualdad estricta, y debe definirse explícitamente
  • Normalmente se escribe τ₁ <: τ₂ y se lee “τ₁ es subtipo de τ₂”
  • Una relación de subtipado simple puede introducir el tipo superior ⊤ y el tipo inferior ⊥
    • τ <: τ: todo tipo es subtipo de sí mismo
    • τ <: ⊤: todo tipo es subtipo de ⊤
    • ⊥ <: τ: ⊥ es subtipo de todo tipo
  • La primera regla es la regla reflexiva, y a menudo se abrevia como refl
  • Para permitir subtipado, la relación debe usarse explícitamente en cada regla de tipado que lo admita
    • En la regla de aplicación de funciones, si el tipo del argumento τ₁ es subtipo del tipo del parámetro τ₂, se puede permitir la aplicación

Múltiples contextos y comprobación bidireccional de tipos

  • Algunos sistemas de tipos definen juicios de tipado que incluyen más de un contexto
    • El segundo contexto normalmente se llama Δ
    • Γ;Δ ⊢ e : τ se usa con frecuencia cuando ambos contextos funcionan como entradas
    • Γ ⊢ e : τ ⊣ Δ se usa con frecuencia cuando Δ funciona como salida
  • El segundo contexto se usa de distintas maneras según el propósito
    • Puede hacer que ciertas variables solo puedan referenciarse dentro de una determinada expresión
    • En lenguajes de programación conscientes de recursos, puede usarse como contexto de salida para rastrear qué variables se consumieron
  • La comprobación bidireccional de tipos es un enfoque que realiza inferencia de tipos no local limitada sin un resolvedor de restricciones
  • Un sistema bidireccional divide el juicio general Γ ⊢ e : τ en dos juicios especializados
    • Γ ⊢ e ⇐ τ: juicio de comprobación (checking) que verifica si la expresión e tiene el tipo esperado τ; algorítmicamente, τ es una entrada
    • Γ ⊢ e ⇒ τ: juicio de inferencia (inference) usado cuando no hay información de tipo esperada; algorítmicamente, τ es una salida
  • Los dos juicios se definen de manera mutuamente recursiva para transmitir información de tipos en ambas direcciones
  • Con este método se pueden omitir algunas anotaciones de tipo, y la regla de comprobación de una abstracción lambda puede obtener el tipo del parámetro a partir del tipo de función esperado, por lo que puede omitirse la anotación del binder de variable

Lecturas relacionadas

1 comentarios

 
GN⁺ 2023-08-17
Opiniones en Hacker News

  • Guy Steele dio una charla sobre este tema hace tiempo. Incluso les puso nombres buscables a algunas notaciones, como diagramas bidimensionales de reglas de inferencia.
    Él lo llama metanotación de ciencias de la computación, aunque personalmente me parece más cercano a la teoría de lenguajes de programación. https://m.youtube.com/watch?v=dCuZkaaou0Q

  • Esta notación se remonta hasta Frege. Es difícil buscarla si no sabes qué buscar, pero este artículo parece un resumen bastante bueno: https://plato.stanford.edu/entries/frege-logic
    El símbolo de torniquete |- ya se usaba, y la línea horizontal que en clase llamaban “Fregescher Schlussstrich”, es decir, la raya de conclusión de Frege, originalmente parece haber sido parte del propio torniquete y luego se convirtió en un elemento separado en la notación moderna.

    • “Schlussstrich” probablemente se traduciría mejor como raya de deducción o raya de inferencia.

  • Types and Programming Languages, de Benjamin C. Pierce, es un buen libro de texto que cubre estos temas.

    • Es irónico que TAPL sea bastante poco claro al explicar el significado básico de la sintaxis que él mismo usa. Esta respuesta es varios órdenes de magnitud más clara que TAPL.

  • Aunque estudié ciencias de la computación, todavía me confunde la diferencia de significado entre |– y |=, y en qué nivel de metasintaxis está cada una de las variables usadas.
    Irónicamente, una de las causas es que la notación en sí no tiene tipos explícitos.

  • Para quien esté dudando si leerlo: este artículo explica la notación de sistemas de tipos que aparece en papers de ciencias de la computación y, en la práctica, es una introducción a la notación BNF para sistemas de tipos, reglas de inferencia, etc.
    Parece un buen resumen.

    • Sinceramente, lo único que necesito es una chuleta que diga cómo leer los símbolos como palabras en inglés.
      Entiendo el concepto lógico de la aplicación de tipos, pero como no leo papers de ciencias de la computación con frecuencia, no termino de fijar en la cabeza la correspondencia entre símbolos y significado.
    • Que este tipo de cosas se haya abstraído exhaustivamente durante años muestra un rasgo muy propio de las ciencias de la computación.

  • En uno de los ejemplos, 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 significa “𝗍𝗋𝗎𝖾+2 es de tipo 𝖨𝗇𝗍”, pero se dice que es aún más raro porque la expresión 𝗍𝗋𝗎𝖾+2 en sí no tiene sentido y tampoco tiene tipo.
    Sin embargo, en Python, True + 2 efectivamente es un entero y su valor es 3. Más allá de si debería ser así o no, de hecho lo es.

    • Si crees que True + 2 tiene sentido, basta con definir directamente una regla de juicio que lo permita.
      La lógica y la teoría de sistemas de tipos no se preocupan por cuáles axiomas y reglas de inferencia uses; solo permiten razonar sobre esas reglas y sus interacciones. Por ejemplo, puedes poner |- True : Bool, |- True : Int, o, si quieres permitirlo solo en ciertas expresiones, hacer que de |- x : Int se derive |- True + x: Int.
    • ¿No depende esto del lenguaje? Por ejemplo, en C true se mapea a 1, así que true+1=2.
    • Aunque True + 2 no arroje error en Python o C, sigue siendo una tontería porque hace que la semántica del lenguaje sea más difícil de razonar solo para darle al programador un poco de azúcar sintáctica.

  • Buenísimo. Durante años tuve curiosidad por esto, pero no sabía qué términos de búsqueda usar para investigarlo más.

  • A veces molesta un poco cuando alguien libera gratis conocimiento arcano que a uno le costó aprender ;) Ojalá hubiera existido un artículo así cuando yo estaba aprendiendo esto. Espero que, al hacerlo más accesible, haya menos lenguajes desastrosos.

  • Al leer el Ada Reference Manual, reconocí de inmediato este tipo de sintaxis. No sabía cómo se llamaba, pero me pareció interesante verla en un caso de uso real, y todo el lenguaje está definido con esa notación.
    Ej.: https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax

  • Este parece un buen lugar para predicar una de esas causas que decidí defender hasta el final. En el formato de anotación de tipos que usa dos puntos, los espacios a ambos lados de los dos puntos deberían ser iguales.
    Para mí, por casualidad existen dos símbolos distintos que tienen la misma forma, es decir, dos puntos. Uno es el dos puntos de etiqueta, en el que la parte anterior introduce la posterior, como en inglés, o lo de la izquierda es una etiqueta para lo de la derecha; ahí entran el inicio de bloques en Python, los pares clave-valor y los pares nombre-valor de structs en C o Rust.
    El otro es una anotación de tipos tomada de las matemáticas. Es una relación binaria, y las relaciones binarias llevan el mismo espacio a izquierda y derecha. Así como no escribimos x= 1, x> y ni x+ z, lo natural no sería escribir x: X, sino x : X.
    Cuando veo a: b, lo leo de inmediato como dos puntos de etiqueta, y si es una anotación de tipo, cada vez necesito una conversión mental adicional, muy pequeña. Estoy hablando de sintaxis de lenguajes de programación, y personalmente prefiero mucho más x : X que X x.
    [1] “Evangelion” es una palabra genial que viene de εὐαγγέλιον, es decir, “buena noticia”. [2] https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...

    • Puede haber algunos malentendidos. En la escritura matemática también aparece efectivamente la notación f: X->Y, con más espacio a la derecha de los dos puntos; de 3 libros que revisé, 1 usaba solo esa notación.
      Además, eso sigue siendo más bien una forma de etiquetado: etiqueta una función de una forma específica. En matemáticas, cuando los dos puntos se usan con un significado realmente distinto es como abreviatura de such that; por ejemplo, aparece a menudo en definiciones de conjuntos como { x : x \in IN and x | 2} o junto con cuantificadores.
    • Es una perspectiva interesante. Lo que dices sobre el paso mental adicional es lo mismo que siento cuando leo la notación común X x. x: X me resulta mucho más natural y se siente más cercano al modo en que se usan los dos puntos en el lenguaje natural.
      Hay una proposición y lo que viene después de los dos puntos la explica con más detalle; en ese sentido, el tipo encaja perfecto como información adicional sobre lo que está a la izquierda.
    • En teoría de tipos, creo que la práctica estándar suele ser dejar el mismo espacio a ambos lados de los dos puntos, como t[espacio]:[espacio]T.
      La teoría de tipos en general tiene aspectos de caos e inconsistencia, pero este caso es una de esas raras ocasiones en que todos son bastante consistentes. Me dio curiosidad ver cómo lo escribía yo en la licenciatura, y resulta que también lo dejé bonito y simétrico: https://dvt.name/logic/horse2.pdf
    • x: X corresponde al uso en el que “después de los dos puntos viene una explicación”.
      Es decir, algo como variable x: It’s an X.
    • age: int se puede leer fácilmente en inglés como “person’s age: an integer”.
      Por eso los dos puntos nunca me han molestado demasiado.