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.

翻译：类型状态系统因其需要复杂的别名追踪机制而声名狼藉。我们为不纯函数式编程环境下的类型状态提出了一种新的、面向转换的基础理论。我们的方法依赖于有序类型进行简单的别名追踪，其形式化借鉴了束蕴涵的相关工作。尽管如此，我们支持在类型状态存在的情况下一种灵活的借用概念。我们的核心演算引入了一种由有序偏幺半群索引的资源类型概念，该幺半群用于建模抽象状态转换。我们证明了相对于资源插桩语义的语法类型可靠性。我们给出了类型系统的算法版本并证明了其可靠性。算法类型化促成了一个简单的表层语言，该语言无需暴露有序类型的繁琐细节。我们为表层语言实现了一个类型检查器，并为核心语言实现了一个解释器。