Linear Haskell: practical linearity in a higher-order polymorphic language
FOS: Computer and information sciences
Computer Science - Programming Languages
Functional languages
linear types
02 engineering and technology
polymorphism
[INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
Formal language definitions
laziness
Haskell
linear logic
0202 electrical engineering, electronic engineering, information engineering
GHC
Programming Languages (cs.PL)
DOI:
10.1145/3158093
Publication Date:
2017-12-29T14:21:49Z
AUTHORS (5)
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.
SUPPLEMENTAL MATERIAL
Coming soon ....
REFERENCES (36)
CITATIONS (68)
EXTERNAL LINKS
PlumX Metrics
RECOMMENDATIONS
FAIR ASSESSMENT
Coming soon ....
JUPYTER LAB
Coming soon ....