一句话：为 Scala 3 设计一等精化类型，使精化与子类型、推断、模式匹配统一整合，并机化证明核心演算的类型可靠性。
精化类型（用逻辑谓词限定的类型）在 Liquid Haskell、F*、Dafny 中已用于轻量级验证，但精化常写在独立规约语言中或被视为二等注解，与宿主类型系统脱节，也无法参与类型推断、子类型与重载。本文为 Scala 3 提出一等精化类型：精化即普通类型，参与子类型、推断与模式匹配。作者在 Rocq 中机化证明了一个纯核心演算的可靠性，该演算含依赖函数类型、有界多态、正等递归类型、并/交类型与精化类型，采用燃料有界定义解释器与语义类型化；部分正确性语义允许谓词发散，证明不依赖终止性假设。设计已实现为 Scala 3 编译器原型扩展，并配有基于 e-graph 的谓词蕴含求解器。
Refinement types—types qualified with logical predicates—have proven effective for lightweight verification in languages like Liquid Haskell, F*, and Dafny. However, in these systems refinements are either written in a separate specification language or treated as second-class annotations, disconnected from the host language's type system. This disconnect creates usability barriers: programmers must maintain two mental models, and refinements cannot interact with features like type inference, subtyping, or overloading. We present the design of first-class refinement types for Scala 3, where refinements are ordinary types that participate in subtyping, inference, and pattern matching alongside existing language features. We prove type soundness of a core, pure calculus mechanized in Rocq, combining dependent function types, bounded polymorphism, positive equi-recursive types, union and intersection types, and refinement types, using a fuel-bounded definitional interpreter and semantic typing. A distinctive design choice is our partial-correctness semantics: predicates are arbitrary terms that may diverge, and type soundness requires no termination assumptions. Finally, we implement our design as a prototype extension of the Scala 3 compiler with a lightweight e-graph-based solver for predicate entailment.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2605-08369,
title = {First-Class Refinement Types for Scala},
author = {Matt Bovel and Viktor Kunčak and Martin Odersky},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839541}
}