通过计算设计类型检查器：The Calculated Typer

The Calculated Typer

Source | HN Comments

该论文提出了一种基于计算的方式设计类型检查器，核心是通过等式推理从行为规范中推导出类型检查器。研究者展示了如何利用 fold fusion 等代数方法简化计算，并通过约束方法求解和组合 fusion 前置条件来改进设计。论文通过三个例子阐述了该方法，包括一个简单的表达式语言、支持异常的语言以及 lambda calculus 的一个版本。

The Calculated Typer：一种计算式类型检查器设计方法

Zac Garby, Patrick Bahr 和 Graham Hutton

提交同行评审，2025年2月。

摘要

我们提出了一种计算式方法来设计类型检查器，展示了如何使用等式推理从行为规范中推导出它们。此外，我们还展示了如何通过基于 fold fusion 的代数方法来简化计算，并通过基于约束的方法来求解和组合 fusion 前置条件，从而进一步改进计算。我们用三个复杂度递增的例子来说明我们的方法：首先是一个简单的表达式语言，然后添加对异常的支持，最后考虑一个版本的 lambda calculus。

分类: Type Systems, Formal Verification

标签: Program Calculation, Type Checker

bib Paper