Teoría de corte de tipos bidireccional para depuración de errores

El artículo 'Bidirectional Type Slicing', publicado en arXiv, presenta una teoría formal para explicar el origen de los tipos en programas de software. A diferencia de las herramientas de desarrollo actuales, que solo informan qué tipo tiene una expresión, este enfoque permite a los programadores responder preguntas de 'por qué' sobre la tipificación, proporcionando un programa parcial minimizado que reproduce el tipo consultado. La teoría se centra en sistemas de tipos bidireccionales, distinguiendo entre la síntesis (qué tipo genera un término) y el análisis (qué tipo espera el contexto). Los autores desarrollan un cálculo central con agujeros, productos, sumas y polimorfismo explícito, basado en los calculi Hazelnut y marcado lambda. Se demuestra que cada consulta tiene un corte mínimo y que refinar la consulta monótonamente reduce el tamaño del corte. Además, se integra esta teoría con la teoría de marcado de errores, extendiendo la aplicación a programas incompletos o erróneos. El trabajo incluye la mecanización de la metateoría en Agda y la implementación de una aproximación lineal de tiempo en el entorno de programación Hazel. Esta herramienta facilita la depuración de errores de tipos y la refactorización, ya que permite identificar exactamente qué partes del código son relevantes para un error específico, eliminando el ruido de código irrelevante.