Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, Arnaud Spiwack
2017 · arXiv
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.
Metadata: arXiv. Abstracts retain their original authors’ rights.
Original HN comments, with labels from simple text rules. A label describes the whole comment and may miss context or irony. Read the discussion to make up your own mind. About the labels
5 selected excerpts · 5 total mentions
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 https://arxiv.org/pdf/1710.09756.pdf
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 https://arxiv.org/pdf/1710.09756.pdf for details.
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 use-after-free errors. Also, linear-typed arrays can perform in-place updates if there are no external pointers to the data. Similar to linear types is the affine type, where a value is used at-most once. Rust's borrow checker is based on this notion, so that values are "moved" rather than "copied". [1] https://en.wikipedia.org/wiki/Uniqueness_type [2] https://en.wikipedia.org/wiki/Substructural_type_system [3] https://clean.cs.ru.nl/Clean [4] https://arxiv.org/abs/1710.09756
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/ https://github.com/apple/swift/blob/master/docs/OwnershipMan... https://dlang.org/blog/2019/07/15/ownership-and-borrowing-in... "Linear Haskell", https://arxiv.org/abs/1710.09756 In the context of Rust, maybe showing lifetimes graphically in an IDE would help productivity versus languages that offer automatic memory management alongside ownership.
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 article (described as channel-passing). [1] https://arxiv.org/abs/1710.09756 [2] https://www.youtube.com/watch?v=t0mhvd3-60Y
More from the same topics.
Haoran Xu, Fredrik Kjolstad
Fast compilation is important when compilation occurs at runtime, such as query compilers in modern database systems and WebAssembly virtual machines in modern browsers.
Ross Mcilroy, Jaroslav Sevcik, Tobias Tebbi +2
The recent discovery of the Spectre and Meltdown attacks represents a watershed moment not just for the field of Computer Security, but also of Programming Languages.
Daniel Ingalls
This paper presents a personal view of the evolution of six generations of Smalltalk in which the author played a part, starting with Smalltalk-72 and progressing through Smalltalk-80 to Squeak and Etoys.
Donald E. Knuth