一句话：提出面向不纯函数式编程、基于有序类型与有序偏幺半群资源类型的 typestate 基础，支持灵活借用并证明类型健全性。
Typestate 系统因需跟踪别名而异常复杂。本文在不纯函数式编程中提出一种新的、面向状态迁移的 typestate 基础：用有序类型（ordered types）进行简单的别名跟踪，其形式化借鉴束蕴涵（bunched implications），并在 typestate 下支持灵活的借用。核心演算包含由有序偏幺半群索引的资源类型，用以建模抽象状态迁移。作者证明相对于资源插桩语义的语法类型健全性，给出类型系统的算法化版本并证明其健全性。算法化类型支持简洁的 surface language，隐藏有序类型的繁琐细节。最后实现了该表面语言的类型检查器和核心语言解释器。
Typestate systems are notoriously complex as they require sophisticated machinery for tracking aliasing. We propose a new, transition-oriented foundation for typestate in the setting of impure functional programming. Our approach relies on ordered types for simple alias tracking and its formalization draws on work on bunched implications. Yet, we support a flexible notion of borrowing in the presence of typestate. Our core calculus comes with a notion of resource types indexed by an ordered partial monoid that models abstract state transitions. We prove syntactic type soundness with respect to a resource-instrumented semantics. We give an algorithmic version of our type system and prove its soundness. Algorithmic typing facilitates a simple surface language that does not expose tedious details of ordered types. We implemented a typechecker for the surface language along with an interpreter for the core language.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Saffrich0024,
title = {Law and Order for Typestate with Borrowing},
author = {Hannes Saffrich and Yuki Nishida and Peter Thiemann},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689763}
}