Un rompecabezas de verificación bidireccional de tipos

 (haskellforall.com)
1 puntos por GN⁺ 1 시간 전 | 1 comentarios | Compartir por WhatsApp
  • En la implementación de verificación bidireccional de tipos de Grace, se usaba el tipo del primer elemento de una lista como si fuera el tipo de todos los elementos, lo que hizo que se eliminara el campo port: 8080 y produjera un resultado de evaluación incorrecto
  • El ejemplo problemático recorría una lista con { domain: "google.com" } y { domain: "localhost", port: 8080 }, usando código que asignaba el puerto predeterminado 443, y devolvía [ "google.com:443", "localhost:443" ] en lugar del valor esperado [ "google.com:443", "localhost:8080" ]
  • La inferencia anterior para listas infería primero List { domain: Text } a partir del primer elemento y luego verificaba el resto de los elementos contra ese tipo; durante el proceso de elaboración se eliminaba el campo port porque no existía en el supertipo
  • La implementación corregida infiere primero los tipos de todos los elementos, luego calcula el supertipo más específico y vuelve a verificar cada elemento contra ese tipo para rellenar valores Optional faltantes con null o some
  • Después de la corrección, la lista original se infiere como List { domain: Text, port: Optional Natural }; el port del primer registro pasa a ser null, y el port: 8080 del segundo se conserva como some 8080, devolviendo así el resultado esperado

El bug de inferencia de tipos de listas en Grace

  • Grace usa un sistema de verificación bidireccional de tipos basado en Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, y al acumularse implementaciones que esquivaban las limitaciones de este enfoque, terminó apareciendo un bug extraño
  • El programa problemático recorría la lista authorities, enlazaba domain y port de cada registro, y usaba 443 como valor predeterminado si port no estaba presente, con forma de list comprehension
let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for { domain, port = 443 } of authorities

in  "${domain}:${show port}"
  • El resultado esperado era [ "google.com:443", "localhost:8080" ], pero la versión con el bug devolvía [ "google.com:443", "localhost:443" ], ignorando por completo el campo port: 8080 del segundo registro
  • El problema no estaba en el evaluador, sino en el verificador de tipos; influyeron tanto la inferencia del tipo de la lista como la elaboración realizada durante la verificación de tipos

Verificación bidireccional de tipos y los límites del enfoque anterior para inferir listas

  • El tipo que Grace esperaba para la lista authorities era el siguiente
List { domain: Text, port: Optional Natural }
  • Este tipo significa que cada registro tiene un campo obligatorio domain: Text, y que el campo port: Optional Natural puede estar o no presente
  • Sin embargo, la implementación anterior infería un tipo más estrecho, así
>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }
  • La verificación bidireccional de tipos se divide básicamente en dos tareas
    • Inferir el tipo de una expresión
    • Verificar si una expresión coincide con un tipo esperado
  • Solo con estas dos tareas, no es fácil combinar los tipos de varios elementos de una lista para construir el supertipo de los elementos de la lista completa
  • La implementación anterior de Grace infería el tipo de una lista de la siguiente manera
    • Infería el tipo del primer elemento de la lista
    • Verificaba que todos los elementos restantes coincidieran con el tipo inferido a partir del primer elemento
  • Como el tipo del primer elemento { domain: "google.com" } era { domain: Text }, ese mismo tipo pasaba a ser el tipo de todos los elementos de la lista
  • Si se quería otro tipo, había que agregar una anotación de tipo explícita, pero el JSON real que Grace pretende manejar puede tener esquemas grandes y complejos, así que no querían obligar a escribir todo el esquema como una enorme anotación de tipo

Por qué la elaboración también cambió el resultado de la evaluación

  • El verificador de tipos de Grace no solo detecta errores de tipo; también realiza elaboración para ajustar expresiones durante el proceso de verificación
  • Cuando se verifica un subtipo contra un supertipo y ambos tipos no coinciden, el verificador inserta coerciones explícitas
  • Internamente, el evaluador de Grace representa todos los valores Optional como valores etiquetados con null o some x
  • Si se coloca un valor sin etiqueta donde se espera un Optional, Grace inserta automáticamente la etiqueta some
>>> [ some 1, 2 ]  # This would be a type mismatch without elaboration
[ some 1, some 2 ]
  • Si el tipo del primer elemento se infiere como Optional Natural y el segundo elemento es un Natural sin etiqueta, el verificador de tipos inserta la etiqueta some en lugar de producir un error de incompatibilidad de tipos
  • Lo mismo ocurre con los registros, y Grace admite subtipado de registros, por lo que coacciona los registros para ajustarlos al supertipo
>>> { x: 1, y: true }: { x: Natural }
{ "x": 1 }
  • Si se anota un registro con un tipo de registro más pequeño, el verificador de tipos lo permite y elimina los campos que no existen en el supertipo
  • Incluso al evaluar solo la lista authorities, la implementación anterior eliminaba el campo port de la siguiente manera
>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com" }, { "domain": "localhost" } ]
  • Este resultado se producía por el siguiente flujo
    • Se infería el tipo del primer elemento como { domain: Text }
    • El segundo elemento se verificaba contra ese tipo esperado
    • El segundo elemento coincidía con ese tipo, pero tenía un campo extra port
    • El verificador de tipos eliminaba el campo port para ajustarlo al tipo esperado
  • La coerción de registros en sí no era la causa de fondo; el problema real era que la inferencia del tipo de listas trataba el tipo del primer elemento como si fuera el tipo de toda la lista

La solución: calcular el supertipo más específico

  • Grace agregó una nueva operación para inferir correctamente el tipo total de una lista
  • La nueva operación calcula el supertipo más específico (most-specific supertype), es decir, la cota superior mínima (least upper bound), de dos tipos
  • Que C sea un supertipo de A y B significa que C es supertipo tanto de A como de B
  • Que C sea el supertipo más específico de A y B significa que C es subtipo de cualquier otro supertipo de A y B
  • Con esta nueva operación, la inferencia del tipo de listas cambió al siguiente orden
    • Inferir el tipo de cada elemento de la lista
    • Calcular el supertipo más específico de todos los tipos de los elementos
    • Verificar que cada elemento coincida con ese supertipo más específico
    • Devolver ese supertipo más específico como el tipo de los elementos de toda la lista
  • Con este enfoque, la siguiente lista infiere correctamente su tipo
>>> :type [ { x: 1 }, { y: true } ]
List { x: Optional Natural, y: Optional Bool }
  • El flujo interno es el siguiente
    • { x: 1 } se infiere con tipo { x: Natural }
    • { y: true } se infiere con tipo { y: Bool }
    • El supertipo más específico de ambos tipos pasa a ser { x: Optional Natural, y: Optional Bool }
    • Luego cada elemento se verifica contra ese supertipo
  • La razón para volver a verificar cada elemento contra el supertipo es aplicar la elaboración correcta, como rellenar some y null faltantes
>>> [ { x: 1 }, { y: true } ]
[ { "x": some 1, "y": null }, { "y": some true, "x": null } ]

El tipo y el resultado de evaluación de authorities después de la corrección

  • Tras corregir el verificador de tipos, la lista original authorities ahora infiere el tipo esperado
>>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
List { domain: Text, port: Optional Natural }
  • El resultado evaluado y elaborado también conserva port como campo opcional
>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com", "port": null }
, { "domain": "localhost", "port": some 8080 }
]
  • El port faltante del primer registro se rellena con null, y el port: 8080 del segundo se conserva como some 8080
  • El ejemplo original de list comprehension también devuelve ahora el resultado esperado
[ "google.com:443", "localhost:8080" ]

Soporte para JSON y la elección de complejidad de implementación

  • La razón por la que Grace insiste tanto en la verificación bidireccional de tipos es que considera que este enfoque, aunque complejo, es un marco de verificación de tipos lo bastante potente como para inferir tipos de JSON reales
  • La inferencia Hindley-Milner, o marcos de verificación de tipos más simples y parecidos, tienen dificultades para manejar las formas que aparecen en datos JSON reales
  • Grace no fue creado como un lenguaje ergonómico exclusivamente para trabajar con JSON, pero tampoco ignoró el soporte para JSON
  • A partir de la experiencia con Dhall, se tomó en cuenta que los usuarios son sensibles a una interoperabilidad ergonómica con JSON, y por eso la sintaxis y el sistema de tipos de Grace se diseñaron considerando la compatibilidad con JSON, incluso si eso aumentaba la complejidad de implementación

Material relacionado que vale la pena revisar

  • Datatype unification using Monoids: trata un algoritmo de inferencia de tipos para tipos de datos simples, esencialmente equivalente al algoritmo que Grace usa para calcular el supertipo más específico
  • The appeal of bidirectional typechecking: explica por qué vale la pena aprender verificación bidireccional de tipos si se quiere implementar un lenguaje que use subtipado de alguna forma
  • Local Type Inference: uno de los artículos pioneros sobre verificación bidireccional de tipos, citado aquí como origen de técnicas como la cota superior mínima y la elaboración de expresiones hacia un lenguaje interno

Apéndice: por qué hace falta la coerción de registros

  • La siguiente expresión en Grace muestra por qué es necesaria la coerción de registros
let f (input: { }) = input.x

in  f { x: 1 }
  • Si esta expresión se aceptara en la verificación de tipos, surgiría el problema de cuál debería ser el tipo de retorno de f
  • El tipo de retorno no debería ser Natural
let f (record: { }): Natural = record.x  # WRONG: type error

in  f { x: 1 }
  • f recibe input con el tipo de registro vacío { }, así que no puede extraer un valor Natural de ese registro
  • Aunque en la llamada se le pase casualmente un registro con un campo x, la función f debe funcionar para cualquier entrada del tipo { }
  • También sería una decisión sólida que el verificador de tipos rechazara accesos a campos que no existen en el tipo de entrada declarado, pero entonces se perdería una capacidad necesaria para manejar datos JSON reales
  • El ejemplo original de authorities es, en esencia, equivalente al siguiente azúcar sintáctico
let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for authority of authorities

let default = fold{ some port: port, null: 443 }

in  "${authority.domain}:${show (default authority.port)}"
  • Si se rechazara el acceso a campos faltantes, no sería posible enlazar campos potencialmente ausentes ni tratarlos con valores predeterminados
  • La decisión de diseño para manejar bien datos JSON reales fue la siguiente
    • Si falta un campo, devolver null
    • Asignar al tipo de acceso forall (a: Type) . Optional a
  • Este tipo es un tipo que solo puede contener null
  • Si se adopta este enfoque, entonces es obligatorio eliminar de un registro los campos que no existan en el supertipo
  • Si no se eliminaran los campos extra, el siguiente ejemplo devolvería 1 : forall (a: Type) . Optional a
let f (input: { }) = input.x

in  f { x: 1 }
  • Eso produciría una expresión mal tipada en la que 1 aparece dentro de un tipo que solo debería poder contener null
  • Una expresión incorrecta así incluso podría romper el evaluador
let f (input: { }) = input.x  # Inferred type: forall (a: Type). Optional a

let default (input: Optional Text) = fold{ some text: text, "" }

in  "${default (f { x: 1 })}!"  # Runtime error if `f` returns `1`
  • En Grace, que busca manejar datos JSON reales, coaccionar explícitamente los registros para ajustarlos al supertipo es un comportamiento razonable, y el bug real no estaba en la coerción, sino en la solución temporal anterior para inferir tipos List

Lecturas relacionadas

1 comentarios

 
GN⁺ 1 시간 전
Comentarios en Lobste.rs

  • Es motivo de felicitación haber tomado el paper Complete And Easy y haberlo llevado a una forma que realmente funciona. También es un buen ejemplo de cómo la naturaleza codiciosa de la verificación bidireccional de tipos puede generar problemas sutiles
    No lo digo como crítica; la inferencia siempre trae problemas y al final se parece más a elegir con cuáles problemas estás dispuesto a vivir. Por eso, personalmente considero que el subtipado y las conversiones forzadas de tipos suelen acercarse a un antipatrón
    Si tomas los datos como la fuente de verdad del tipo, se vuelve más difícil verificar si los datos están mal y, como en el ejemplo, terminas obteniendo un tipo incorrecto en lugar de un error útil. Dicho eso, como esto viene de la persona que hizo Dhall, seguramente sabe mucho más del tema que yo. La idea de generar un esquema a partir de varios datos sí parece digna de investigación, aunque no estoy seguro de llamarle “verificación de tipos”, dado que normalmente se piensa en los tipos como algo prescriptivo más que descriptivo

  • No entiendo bien por qué no simplemente rechazan f. Estás accediendo a un campo en un registro de un tipo que nunca podría tener ese campo, así que casi con certeza es un bug del programa y parece una situación en la que el verificador de tipos debería avisarte
    La diferencia con el ejemplo de authority es que no falta el tipo de port, sino que es Optional. Rechazar campos ausentes no implica que también haya que rechazar campos opcionales. Si ya estás forzando valores con base en el tipo, entonces { domain: "google.com" } también podría convertirse forzosamente al valor { domain: "google.com", port: null }

    • En resumen, no hay necesidad de rechazar f; eso es una restricción innecesaria. Me parece estrictamente mejor que un acceso incorrecto a un campo devuelva null : forall (a : Type) . Optional a a que se rechace ese acceso incorrecto
      Permite más programas válidos, y los programas mal tipados igual siguen fallando. Por ejemplo, un programa que intente usar el valor accedido sin manejar null seguiría dando un error de tipos

  • Lo primero que se me ocurre es que los row types resuelven esto. Supongo que ya lo habrán considerado. ¿Aquí el problema es que los row types se rompen al interactuar con el subtipado?

    • Grace tiene row types y polimorfismo de filas. En Grace a las filas les llaman “fields”, pero fuera de eso es exactamente lo mismo
      De hecho, el algoritmo del supertipo más específico también toma en cuenta los row types
      Por ejemplo, si escribes algo así: 
      \\record0 record1 ->

let _ = record0.x

let _ = record1.y

in  [ record0, record1 ]
      Grace infiere el siguiente tipo para esta expresión: 
      forall (a : Type) .  
forall (b : Type) .  
forall (c : Fields) .  
  { x: b, y: a, c } -> { y: a, x: b, c } -> List { x: b, y: a, c }

  • ¿No es este un ejemplo del problema de instanciación codiciosa que se menciona en la sección 5.1.1 del paper Bidirectional Typing?
    “Fue bastante desafortunado que, en la configuración original, este enfoque codicioso fuera sensible al orden de los argumentos. Sin embargo, puede funcionar en un entorno de polimorfismo predicativo de alto rango sin otras formas de subtipado. El ‘tabby-first problem’ no puede surgir, porque la única forma en que un tipo puede hacerse estrictamente menor es volviéndose estrictamente más polimórfico, y si el primer argumento fuera polimórfico entonces habría que instanciar 𝛼 con un tipo polimórfico, lo cual violaría la predicatividad”