Linear Haskell
Linear Haskell
复制标题
DOI：
10.1145/3158093
复制
发表时间：
2018-01-01
影响因子：
1.8
通讯作者：
Spiwack, Arnaud
中科院分区：
文献类型：
--
作者：
Bernardy, Jean-Philippe;Boespflug, Mathieu;Spiwack, Arnaud
线性类型系统有着悠久而传奇的历史，但与OCaml或Haskell等现有语言集成的道路并不清晰。在本文中，我们研究了一个线性类型系统，该系统在设计时考虑了两个关键属性：向后兼容性和跨库的线性和非线性用户的代码重用。只有这样，线性类型的好处才能渗透到传统的函数式编程中。我们不是将类型分为线性和非线性对应，而是将线性附加到函数箭头上。线性函数可以接受线性边界值的输入，但也可以对不受限制的常规值进行操作。为了证明我们的线性类型系统的有效性——既可以很容易地集成到现有的语言实现中，也可以简化用线性类型编写程序——我们在GHC（领先的Haskell编译器）中实现了我们的类型系统，并演示了线性类型的两种应用：具有纯接口的可变数据；并在I/ o执行功能中强制执行协议。
Linear type systems have a long and storied history, but not a clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study a linear type system designed with two crucial properties in mind: backwards-compatibility and code reuse across linear and non-linear users of a library. Only then can the benefits of linear types permeate conventional functional programming. Rather than bifurcate types into linear and non-linear counterparts, we instead attach linearity to function arrows. Linear functions can receive inputs from linearly-bound values, but can also operate over unrestricted, regular values.To demonstrate the efficacy of our linear type system - both how easy it can be integrated in an existing language implementation and how streamlined it makes it to write programs with linear types - we implemented our type system in GHC, the leading Haskell compiler, and demonstrate two kinds of applications of linear types: mutable data with pure interfaces; and enforcing protocols in I/O-performing functions.