一句话：提出 ML 扩展 Affe，以 kind 和约束类型实现线性/仿射资源管理与借用，且无需表达式内线性注解并保留完整主类型推断。
系统编程常需操作文件句柄、网络连接或动态内存等资源，程序员必须遵守特定协议，否则会导致类型不匹配、数据竞争、释放后使用和内存泄漏等缺陷，甚至安全漏洞。静态类型语言虽保证类型可靠性与内存安全，却大多不处理资源的不当使用。线性/仿射类型可强制单线程式资源使用，但现有支持语言通常需要大量类型注解。本文提出 Affe：ML 的扩展，通过 kind 和约束类型管理线性与仿射性质，并受 Rust 启发支持仿射资源的独占与共享借用。Affe 保持 ML 族的不纯、严格函数式表达语言特性，具有完整主类型推断和类型抽象，表达式无需线性注解，并支持常见函数式编程惯用法。
Systems programming often requires the manipulation of resources like file handles, network connections, or dynamically allocated memory. Programmers need to follow certain protocols to handle these resources correctly. Violating these protocols causes bugs ranging from type mismatches over data races to use-after-free errors and memory leaks. These bugs often lead to security vulnerabilities. While statically typed programming languages guarantee type soundness and memory safety by design, most of them do not address issues arising from improper handling of resources. An important step towards handling resources is the adoption of linear and affine types that enforce single-threaded resource usage. However, the few languages supporting such types require heavy type annotations. We present Affe, an extension of ML that manages linearity and affinity properties using kinds and constrained types. In addition Affe supports the exclusive and shared borrowing of affine resources, inspired by features of Rust. Moreover, Affe retains the defining features of the ML family: it is an impure, strict, functional expression language with complete principal type inference and type abstraction. does not require any linearity annotations in expressions and supports common functional programming idioms.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1908-09681,
title = {Kindly bent to free us},
author = {Gabriel Radanne and Hannes Saffrich and Peter Thiemann},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3408985}
}