Linear Haskell: practical linearity in a higher-order polymorphic language

Jean-Philippe Bernardy (1) , Mathieu Boespflug (2) , Ryan R. Newton (3) , Simon Peyton Jones (4) , Arnaud Spiwack (5, 6, 2)

1 GU - Göteborgs Universitet = University of Gothenburg
2 Tweag I/O
3 Indiana University [Bloomington]
4 Microsoft - Microsoft Research [Cambridge]
5 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
6 PI.R2 - Design, study and implementation of languages for proofs and programs

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.

Mots clés: linear logic; laziness; Haskell; polymorphism; linear types; Functional languages; Formal language definitions; GHC

Domaines: Langage de programmation [cs.PL]

Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, Arnaud Spiwack. Linear Haskell: practical linearity in a higher-order polymorphic language. Proceedings of the ACM on Programming Languages, 2017, 2 (POPL), pp.1-29. ⟨10.1145/3158093⟩. ⟨hal-01673536⟩