HackerPapers

arXiv:1710.09756cs.PL

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

Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, Arnaud Spiwack

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.

arXiv comments
Journal reference
DOI
doi:10.1145/3158093
Subjects
cs.PLProgramming Languages

On Hacker News

Linked by 6 identifiable commenters in 6 comments across 4 threads, from Oct 2018 to Dec 2020. Found in 1 HN submission from Nov 2017 to Nov 2017. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments4 threads

  1. GHC 9.0, supporting linear types 3 comments

    • I first became fascinated by linear [1] and uniqueness [2] types with Clean [3], a purely functional language that handles state and IO without monads. This Haskell extension uses linear types for resource safety and scoped effects [4]. For example, linear types can prevent…

      chrisaycockView on HNParent context

    • There is no such thing as a "linear value" per se, since linearity is on the arrow. But speaking of linear values makes sense when there's an ambient monad, and all of the restrictions you expect are enforced; see Section 2.7 (and the last paragraph of Section 6.1) of…

      mauriciocView on HNParent context

    • Good observation. I believe you would use withFADR :: (FragileAndDangerousResource #-> Unrestricted a) -> Unrestricted a One can't tag "linear" values in the type system but one can tag non-linear "unrestricted" values. See "borrow" in Section 7.2, page 5:26 of…

      tomeView on HNParent context

  2. Biscuit: A monolithic, POSIX-subset operating system kernel in Go 1 comment

    • Here is one example, https://github.com/rust-lang/rust/issues/63818 Alternative ideas, here are four, combining the productivity of automatic memory management with ownership, https://swift.org/blog/swift-5-exclusivity/…

      pjmlpView on HNParent context

  3. When Rust is safer than Haskell 1 comment
  4. Rust RAII is better than the Haskell bracket pattern 1 comment

    • Something to keep in mind - linear types are on their way[1], with exactly this usecase in mind. Simon Peyton Jones gave an excellent presentation on the topic[2], briefly discussing exceptions, as well as giving a mention to ResourceT and the phantom type solution in the…

      T-RView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.