重新审视出现类型（Occurrence Typing）的可靠性：语义视角

中文摘要 AI 辅助

在过去的二十年里，众多系统通过限制哪些项可以出现在类型内部，将依赖类型（dependent typing）的某些优势带入了各种新的编程语言。这类技术被称为细化类型（refinement types）、出现类型（occurrence typing）、液体类型（liquid types）和路径依赖类型（path dependent types）等。然而，这些系统所采用的限制常常破坏替换性质（substitution property），因为它们明确禁止在类型内部用任意项替换变量。这导致了这些系统在设计和元理论上的显著复杂性，增加了出现重大错误的可能性。我们考虑了一条特定的出现类型研究路线，即由Tobin-Hochstadt和Felleisen于2010年提出的Typed Racket底层演算。我们表明，类型内替换这一根本性挑战导致了该工作中形式主义和句法类型可靠性定理（syntactic type soundness theorem）的多个缺陷。这些缺陷在基于该工作的其他几篇论文中被复制，并且在Typed Racket本身中也表现为一个可靠性错误（soundness bug）。我们识别并修复了这些问题，修订了Typed Racket的核心演算，并使用在Lean中形式化的步进索引逻辑关系（step-indexed logical relations）给出了一个语义类型可靠性（semantic type soundness）证明。我们认为这种方法比看起来更简单，并且能够轻松扩展以处理Typed Racket中发生类型的复杂性。

英文摘要

Over the past two decades, numerous systems have brought some of the benefits of dependent typing to a wide variety of new programming languages, often by restricting which terms can appear inside types. Such techniques are known as refinement types, occurrence typing, liquid types, and path dependent types, among others. However, the restrictions adopted by these systems often break the substitution property, because they explicitly disallow the ability to substitute arbitrary terms for variables inside types. This leads to significant complexity in the design and metatheory of these systems, increasing the possibility of significant errors. We consider a specific line of work on occurrence typing, namely, the calculus underlying Typed Racket due to Tobin-Hochstadt and Felleisen 2010. We show that the fundamental challenge of substitution into types resulted in multiple flaws in the formalism and the syntactic type soundness theorem of this work. These flaws are replicated in several other papers building on this work, and also surface as a soundness bug in Typed Racket itself. We identify and repair these problems, revising the core calculus of Typed Racket and giving a \emph{semantic type soundness} proof using step-indexed logical relations, formalized in Lean. We argue that this approach is simpler than it may seem, and easily scales to handle the complexity of the occurrence typing in Typed Racket.

发表机构

• Indiana University（印第安纳大学）

机构由 AI 辅助整理，请以论文原文为准。