双向类型切片
Bidirectional Type Slicing
AI总结：
研究开发能解释表达式为何具有特定类型的理论，核心方法是提出双向类型切片，主要贡献为适用于特定双向系统，能证明查询有最小切片并给出计算方法，还可结合错误标记理论解释各类代码中的类型及错误。
AI中文摘要：
开发工具能报告表达式的类型，但无法说明为何是该类型。本文提出类型切片理论：程序员选择一个项，查询其类型信息的任何部分，就能得到一个足以重现查询类型的程序切片。为双向类型系统制定了类型切片，合成切片解释一个项合成的类型，分析切片解释其周围上下文期望的类型。该理论适用于任何配备类型和项精度顺序且满足向下静态渐变属性的双向系统。基于Hazelnut和标记lambda演算，在具有洞、积、和以及显式多态性的核心演算上开发了元理论。证明每个查询都有一个最小切片，细化查询会单调缩小其最小切片。展示了如何精确和近似地计算这些切片。最后，将类型切片与错误标记理论相结合，将结果扩展到任意类型错误的程序，单一机制可解释完整、不完整和错误代码中的类型和类型错误。元理论在Agda中机械化实现，为Hazel编程环境实现了类型切片的线性时间近似。
英文摘要：
Development tools report what type an expression has, but not why it has that type. This paper develops a theory of type slicing: a programmer selects a term, queries any part of its type information, and receives a program slice that is sufficient to reproduce the queried type. We formulate type slicing for bidirectional type systems, where synthesis slices explain the type a term synthesises and analysis slices explain the type expected by its surrounding context. The theory applies to any bidirectional system equipped with precision orders on types and terms satisfying a downwards static graduality property. We develop the metatheory over a core calculus with holes, products, sums, and explicit polymorphism, based on the Hazelnut and marked lambda calculi. We prove that every query has a minimal slice and that refining a query monotonically shrinks its minimal slices. We then show how to calculate these slices both exactly and approximately. Finally, integrating type slicing with error marking theory extends these results to arbitrary ill-typed programs, so a single mechanism explains both types and type errors in complete, incomplete, and erroneous code. The metatheory is mechanised in Agda, and a linear-time approximation of type slicing is implemented for the Hazel programming environment.
