本文提出了双向类型系统的类型切片理论，通过生成足以复现查询类型信息的最小程序切片，解释表达式为何具有特定类型。元理论已在Agda中形式化验证，并为Hazel编程环境实现了线性时间近似算法。
背景
类型系统是编程语言的基础，但IDE和编译器仅报告类型而不解释其来源。双向类型检查被Haskell、Agda等语言采用，结合类型合成与分析以实现更好的错误提示和性能。
- 来源
- Lobsters
- 发布时间
- 2026年10月6日 21:36
- 评分
- 5.0 / 10
本文提出了双向类型系统的类型切片理论，通过生成足以复现查询类型信息的最小程序切片，解释表达式为何具有特定类型。元理论已在Agda中形式化验证，并为Hazel编程环境实现了线性时间近似算法。
类型系统是编程语言的基础，但IDE和编译器仅报告类型而不解释其来源。双向类型检查被Haskell、Agda等语言采用，结合类型合成与分析以实现更好的错误提示和性能。