Idris 2：实践中的定量类型论

导读

这篇论文介绍 Idris 2 编程语言对定量类型理论（Quantitative Type Theory, QTT）的实现。QTT 扩展了线性类型，允许在类型中标注参数的使用次数（如 0 次、1 次或任意次），从而在编译期追踪资源使用并支持运行时擦除。论文报告了把 QTT 落进实际编程语言的设计与工程经验。

HN 关注点：QTT 在真实语言中的落地效果，讨论焦点是线性类型在资源安全 API（如可变数组）上的实际局限。

关键词　Idris 2Quantitative Type Theorydependent typeslinear types

HN 评论精选

这几条评论里：质疑 1　补充 2　亲历 1

亲历Idris 研究者补充实际应用链接，指出 Idris2 自举是依赖类型的大规模实践案例。

你好，我是研究 Idris 的博士生，曾与 Edwin 合作做这项工作。如果想了解更多，或想看 Idris2、依赖类型、QTT 的更多实际应用，这里有几个链接：Idris2 是用 Idris2 写的，所以它是使用依赖类型的大型程序的好例子（GitHub）；我们正在开发一些非常有趣的库；我自己的 Idris 项目包括一个纯声明式的服务器库，你只需给出 API，服务器就完全由你的描述实现和实例化。

lang_agnostic查看英文原文

Hi there, I'm a phd student working on Idris and I used to work with Edwin on this, if you want more info or want to see more practical applications of idris2, Dependent types, or QTT, here are a couple links: - idris2 is written in idris2 so that's a good example of a big program using dependent types https://github.com/idris-lang/Idris2 - we have some very interesting libraries in the works: https://github.com/idris-lang/Idris2/wiki/Libraries - my own projects in idris include a purely declarative server library where you give the API and the server is completely implemented and instantiated from your description https://gitlab.com/avidela/recombine

补充读者分享学习 Idris 的体验，列举书中的依赖类型实用示例，并指出教材基于无 QTT 的 Idris 1。

我正在读《Type-Driven Development with Idris》，强烈推荐（作者就是 Idris 的创造者）。不过它仍基于 Idris 1（没有 QTT）。基础变化不大（部分示例需小改，主要是把以前隐式的参数显式化）。Idris 似乎是一门非常有趣的语言。书中例子包括：类型安全的 printf（编译期检查参数数量和类型）；证明函数是全函数（大致是每个输入都终止）；把无限运行的程序写成动作流，大部分程序可写成全函数，只有消费动作的顶层函数需要是部分函数；用依赖模式匹配的视图以多种方式安全遍历结构；安全除法；定义系统使用的所有效果，而非不受限制的 IO 类型，等等。虽然例子很有趣，但我还没完全理解依赖类型能做的所有事（或有哪些限制），估计需要更多练习。

Tainnor查看英文原文

I'm working through the Type-Driven Development with Idris right now and I can only recommend it (it's written by the creator of Idris). However, it's still based on Idris 1 (which didn't have QTT). The basics haven't changed much though (some examples have to be modified slightly, mostly related to making some arguments explicit that used to be implicit). Idris seems like a really interesting language. Examples from the book include: - typesafe printf (it will check that the correct number of arguments with the correct types are passed at compile time). - proving that functions are total (roughly that means that they terminate for every input) - writing infinitely running programs as a stream of actions, meaning that the majority of the program can be written as a total function and only the top-level function actually consuming the actions needs to be partial - views with dependent pattern matching for traversing structures safely in several ways - safe division - ability to define all the effects your system uses instead of using an unrestricted IO type etc. While the examples are super interesting I don't think that I yet fully grasp all the possible things you could do with dependent types (or what sorts of limitations they have). I guess that would come with more practice.

质疑指出 QTT 的线性只用于参数绑定，不用于类型本身，导致 LinArray 等 API 存在句柄泄漏与双重释放风险，并与 ATS 的设计对比。

我对 QTT 中的线性有点失望，因为我没能想出如何围绕可调整大小的数组创建安全 API。论文中的例子是 LinArray。不幸的是，正如社区发现的，用户可以在 `newArray` 构造函数外“泄漏”一个非线性绑定（该构造函数试图对所有绑定强制线性）。有多个不受限制的句柄时，用户可能意外双重释放（issue #613）。根本问题是 QTT 中的线性是参数绑定的属性，而不是类型本身的属性，所以我们无法轻易把线性表达为类型的全局属性。另一方面，只影响参数绑定使得使用运行时擦除/编译时内容很容易，无需把一堆常见类型重新实现为运行时和编译时专用版本。ATS 选择了另一条路，把线性和运行时擦除作为类型的一部分（但语法开销很大）。

phlip9查看英文原文

I was a bit disappointed with linearity in QTT as I couldn't figured out how to create a safe API around a resizable array. The example given in the paper is a LinArray (https://github.com/idris-lang/Idris2/blob/main/libs/contrib/Data/Linear/Array.idr). Unfortunately, as the community discovered, a user can "leak" a non-linear binding outside of the `newArray` constructor (which is what attempts to enforce linearity for all bindings). With multiple unrestricted handles, a user can accidentally double-free for instance. (https://github.com/idris-lang/Idris2/issues/613) The fundamental issue in this case is that linearity in QTT is a property of the parameter bindings and _not_ the type itself, meaning we can't easily express linearity as a _global_ property of the type. On the other hand, only affecting the parameter bindings makes it really easy to use runtime-erased/comptime stuff without reimplementing a bunch of common types as runtime- and comptime-only versions. ATS chooses the other path and makes linearity and runtime-erasure a part of the type (not without paying a hefty syntactic cost however).

补充读者尝试用自己的话总结：QTT 扩展线性类型以表达状态机等运行时依赖，并求证理解是否正确。

我快速读了论文，大概理解了 10%，比我的平均水平好。我的收获是：线性类型允许表达诸如“此函数不能用空列表调用”的条件；QTT 类型扩展线性类型，允许在类型系统中指定函数之间的运行时依赖。我大致理解了能在类型系统中表达状态机的想法：可以说这个函数只能在这个状态调用，要进入状态必须按顺序调用这些函数。我理解得对吗？这是论文的大致要点吗？

ozmaverick72查看英文原文

I had a quick read of the paper and I think I got about 10% of the content - which is better than my usual average. My take-away - linear types allow you to express conditions such as this function must not be called with an empty list - QTT types extend linear types and allow you to specify run time dependencies between functions in the type system. I got the rough idea of being able to express a state machine in the type system - gives you the ability to say that this function can only be called in this state - to enter the state, these functions must be called in this order. How did I do ? Is that the rough gist of the paper ?

历次讨论

2022Hacker News 讨论帖150 分 · 60 评

HN 二十年，最值得读的论文。

朋友分享的书单

专题阅读路线

本周最多人读

我的书单

必读 30 篇

论文库

这些论文是怎么挑出来的

全量扫一遍

只留论文本身

写导读、译评论

Idris 2：实践中的定量类型论

导读

HN 评论精选

相关资源

历次讨论

同领域还值得读

Google 的软件工程（2017）

Peter Naur：编程作为理论构建 (1985)

SciPy 1.0：Python 科学计算的基础算法

Lisp 的历史（1979）

使用 NumPy 进行数组编程

打赏支持

关注向阳乔木