一句话：提出分级模态类型统一 coeffect 与 graded monad，并在 Granule 中结合线性/索引类型实现定量程序推理。
程序中的数据常作为受使用约束的资源（如文件句柄、通道），而多数语言不检查这些约束，带来正确性挑战。线性类型可区分资源与不受限值，但有界线性逻辑通过索引模态族量化非线性使用，coeffect 类型进一步推广为分级 comonad。本文提出分级模态类型这一统一概念，涵盖 coeffect 类型以及经分级 monad 进行的对偶效应推理；将其与线性类型和索引类型结合，形成可表达定量程序推理的类型理论，从而扩大类型系统可捕获和验证的程序性质范围。作者在完整的函数式语言 Granule 中实现该类型系统，并通过多类示例展示其表达能力。
In programming, some data acts as a resource (e.g., file handles, channels) subject to usage constraints. This poses a challenge to software correctness as most languages are agnostic to constraints on data. The approach of linear types provides a partial remedy, delineating data into resources to be used but never copied or discarded, and unconstrained values. Bounded Linear Logic provides a more fine-grained approach, quantifying non-linear use via an indexed-family of modalities. Recent work on coeffect types generalises this idea to graded comonads, providing type systems which can capture various program properties. Here, we propose the umbrella notion of graded modal types, encompassing coeffect types and dual notions of type-based effect reasoning via graded monads. In combination with linear and indexed types, we show that graded modal types provide an expressive type theory for quantitative program reasoning, advancing the reach of type systems to capture and verify a broader set of program properties. We demonstrate this approach via a type system embodied in a fully-fledged functional language called Granule, exploring various examples.
@article{paperbot607,
title = {Quantitative program reasoning with graded modal types},
author = {Dominic Orchard and Vilem-Benjamin Liepelt and Harley Eades III},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341714}
}