Name
Abstract | ||
|---|---|---|
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.
|
Year | DOI | Venue |
|---|---|---|
2018 | 10.1145/3158093 | Proceedings of the ACM on Programming Languages |
Keywords | DocType | Volume |
GHC,Haskell,laziness,linear logic,linear types,polymorphism,typestate | Journal | 2 |
Issue | ISSN | Citations |
POPL | 2475-1421 | 3 |
PageRank | References | Authors |
0.56 | 19 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jean-Philippe Bernardy | 1 | 120 | 12.33 |
| Mathieu Boespflug | 2 | 3 | 0.56 |
| Ryan Newton | 3 | 802 | 70.80 |
| Simon L. Peyton Jones | 4 | 5036 | 381.19 |
| Arnaud Spiwack | 5 | 91 | 7.04 |