Elaboradores Bidireccionales Tolerantes a Errores para Herramientas de Desarrollo

El problema fundamental que aborda este artículo es cómo los sistemas de tipos, tradicionalmente diseñados para validar la corrección de programas, pueden adaptarse para proporcionar retroalimentación útil en entornos de desarrollo interactivos, incluso cuando el código es incorrecto o incompleto. Los typecheckers bidireccionales, que distinguen entre inferencia (synth) y verificación (check) de tipos, son una base sólida para esta tarea. Sin embargo, su implementación directa a menudo falla estrepitosamente al encontrar un error, dejando al desarrollador sin información contextual crítica. La tesis es que, al adoptar principios de tipado gradual y una abstracción explícita de 'patrones' para la deconstrucción de tipos, se puede construir un elaborador bidireccional que siempre produce un Árbol de Sintaxis Abstracta (AST) anotado, incluso con errores, mejorando drásticamente la experiencia de usuario en IDEs y Language Servers.

Históricamente, los sistemas de tipos han evolucionado desde verificadores batch hasta herramientas más interactivas. La necesidad de retroalimentación continua y rica en errores es un desafío persistente en el diseño de compiladores y herramientas de lenguaje. La integración de la teoría de tipos con la ingeniería de herramientas de desarrollo es un área activa de investigación, con trabajos como los de Cyrus Omar y su equipo en el lenguaje Hazel, que buscan cerrar la brecha entre la corrección formal y la usabilidad práctica.

Arquitectura del Sistema

La arquitectura propuesta se basa en un elaborador bidireccional implementado en OCaml, que utiliza tipos de datos mutuamente recursivos para representar expresiones y tipos. La innovación central es la abstracción de 'patrones' (Get module en la versión con errores, TpView module en la versión tolerante a errores) que encapsula la lógica de deconstrucción y reconstrucción de tipos. Estos patrones permiten que las reglas de tipado se traduzcan a un código más lineal y legible, reduciendo el branching del control de flujo.

En la versión tolerante a errores (ElabNonstop), el sistema utiliza tp option para representar tipos que pueden ser conocidos (Some tp) o desconocidos (None). El módulo TpView proporciona funciones get y put para deconstruir y reconstruir tipos opcionales, respectivamente. Por ejemplo, TpView.arrow.get tp_option siempre devuelve un par de tp option (incluso (None, None) si el tipo de entrada no es una flecha), y TpView.arrow.put (tp1_option, tp2_option) intenta reconstruir un tipo flecha si ambos componentes son conocidos. Esto permite que el elaborador continúe procesando el AST, anotando subexpresiones con None cuando el tipo es irrecuperable, en lugar de detenerse con un error. La función is de TpView se utiliza para verificar explícitamente la forma de un tipo, actuando como un filtro que devuelve None si el tipo no coincide con el patrón esperado. El contexto de tipado (ctx) también se adapta para almacenar tp options, permitiendo la inclusión de variables con tipos desconocidos.

type tp = Bool | Arrow of tp * tp | Tuple of tp list

module Exp = struct
  type var = string
  type 'info exp' =
    | BLit of bool
    | If of 'info t * 'info t * 'info t
    | Lam of var * 'info t
    | App of 'info t * 'info t
    | Annot of 'info t * tp
    | Var of var
    | Let of var * 'info t * 'info t
    | Tuple of 'info t list
    | LetTuple of var list * 'info t * 'info t
  and 'info t = In of ('info * 'info exp')
end

module TpView : sig
  type 'a t = { get : tp option -> 'a; put : 'a -> tp option; }
  val bool : unit option t
  val arrow : (tp option * tp option) t
  val tuple : int -> tp option list t
  val eq : tp option -> unit option t
  val is : 'a t -> tp option -> tp option
end = struct
  type 'a t = { get : tp option -> 'a; put : 'a -> tp option }

  let bool =
    let get tp' = match tp' with Some Bool -> Some () | _ -> None in
    let put tp' = match tp' with Some () -> Some Bool | _ -> None in
    {get; put}

  let arrow =
    let get tp' = match tp' with Some (Arrow(tp1, tp2)) -> (Some tp1, Some tp2) | _ -> (None, None) in
    let put (tp1', tp2') = match tp1', tp2' with Some tp1, Some tp2 -> Some (Arrow(tp1, tp2)) | _ -> None in
    {get; put}

  (* ... other views ... *)

  let is view tp = view.put (view.get tp)
end

Fundamentos Teóricos

La idea de un elaborador que no se detiene ante errores se inspira directamente en el trabajo de Cyrus Omar y sus colaboradores, especialmente en su paper "Total Type Error Localization and Recovery with Holes" (Zhao et al.). Este trabajo adapta el concepto de tipos graduales, introduciendo un tipo 'desconocido' (representado como ?) que es compatible con cualquier otro tipo. Esta 'compatibilidad' es la clave para permitir que el typechecker continúe su ejecución, incluso en presencia de inconsistencias de tipo. El artículo conecta esta compatibilidad con la noción de 'patrones' de Conor McBride, donde la deconstrucción de tipos se convierte en un juicio de compatibilidad en lugar de una igualdad estricta. La teoría de tipos graduales, que combina tipado estático y dinámico, proporciona el marco teórico para manejar la incertidumbre de tipos de manera controlada.