Idris 2：实践中的定量类型论
Idris 2: Quantitative Type Theory in Practice
摘要：
依赖类型允许我们精确地表达函数要做什么。定量类型论（QTT）最近的工作扩展了依赖类型系统的线性，也允许精确表达函数何时可以运行。这是有希望的，因为它表明了设计和推理资源使用协议的能力，例如我们可能会在分布式和并发编程中发现，其中通信信道的状态在整个程序执行过程中都会发生变化。然而，到目前为止，还没有一种完整的程序设计语言来试验这些想法。Idris 2是依赖类型语言Idris的新版本，具有基于QTT的新核心语言，支持线性和依赖类型。在本文中，我们介绍了Idris 2，并描述了QTT如何影响其设计。我们给出的例子，QTT在实践中的好处包括：表示哪些数据在运行时间删除，在类型级别;和，在类型系统中的资源跟踪导致类型安全的并发编程会话类型。
英文摘要：
Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run. This is promising, because it suggests the ability to design and reason about resource usage protocols, such as we might find in distributed and concurrent programming, where the state of a communication channel changes throughout program execution. As yet, however, there has not been a full-scale programming language with which to experiment with these ideas. Idris 2 is a new version of the dependently typed language Idris, with a new core language based on QTT, supporting linear and dependent types. In this paper, we introduce Idris 2, and describe how QTT has influenced its design. We give examples of the benefits of QTT in practice including: expressing which data is erased at run time, at the type level; and, resource tracking in the type system leading to type-safe concurrent programming with session types.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
