research-article

Open access

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

Authors:

Jean-Philippe Bernardy,

Mathieu Boespflug,

Ryan R. Newton,

Simon Peyton Jones,

Arnaud SpiwackAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL

Article No.: 5, Pages 1 - 29

https://doi.org/10.1145/3158093

Published: 27 December 2017 Publication History

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.

Supplementary Material

WEBM File (linearhaskell.webm)

Download
102.29 MB

References

[1]

Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. 2010. Monads Need Not Be Endofunctors. In Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings . 297–311.

Digital Library

[2]

Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O’Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein, and Gernot Heiser. 2016. Cogent: Verifying High-Assurance File System Implementations. In International Conference on Architectural Support for Programming Languages and Operating Systems . Atlanta, GA, USA, 175–188.

Digital Library

[3]

Jean-Marc Andreoli. 1992. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2, 3 (1992), 297–347.

[4]

Robert Atkey. 2017. The Syntax and Semantics of Quantitative Type Theory. (2017). Under submission.

[5]

Erik Barendsen and Sjaak Smetsers. 1996. Uniqueness Typing for Functional Languages with Graph Rewriting Semantics. Mathematical Structures in Computer Science 6, 6 (1996), 579–612.

[6]

J.-P. Bernardy, M. Boespflug, R. R. Newton, S. P. Jones, and A. Spiwack. 2017. Linear Haskell: practical linearity in a higher-order polymorphic language. ArXiv e-prints (Oct. 2017). arXiv: 1710.09756

[7]

Jean-Philippe Bernardy, Víctor López Juan, and Josef Svenningsson. 2015. Composable Efficient Array Computations Using Linear Types. Submitted to ICFP 2015. http://www.cse.chalmers.se/ josefs/publications/vectorcomp.pdf .

[8]

Mathieu Boespflug, Facundo Dominguez, Alexander Vershilov, and Allen Brown. 2014. Project H: Programming R in Haskell. (2014). Talk at IFL 2014.

[9]

Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program. 23, 5 (2013), 552–593.

[10]

Edwin Brady. 2017. Type-driven Development of Concurrent Communicating Systems. Computer Science 18, 3 (2017). https://journals.agh.edu.pl/csci/article/view/1413

[11]

Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus. In Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410 . Springer-Verlag New York, Inc., New York, NY, USA, 351–370.

Digital Library

[12]

Manuel M. T. Chakravarty and Gabriele Keller. 2017. Haskell SpriteKit – Transforming an Imperative Object-oriented API into a Purely Functional One. (2017). http://www.cse.unsw.edu.au/~chak/papers/CK17.html

[13]

Evan Czaplicki. 2012. Elm: Concurrent FRP for functional guis. Senior thesis. Harvard University.

[14]

Stephen Dolan and Alan Mycroft. 2017. Polymorphism, Subtyping, and Type Inference in MLsub. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017) . ACM, New York, NY, USA, 60–72.

Digital Library

[15]

Richard A. Eisenberg and Simon Peyton Jones. 2017. Levity polymorphism. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017 . 525–539.

Digital Library

[16]

Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings . 331–350.

Digital Library

[17]

Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science 50, 1 (1987), 1–101.

Digital Library

[18]

Carl A. Gunter and Didier Rémy. 1993. A proof-theoretic assessment of runtime type errors. Technical Report. AT&T Bell laboratories. Technical Memo 11261-921230-43TM.

[19]

Oleg Kiselyov and Chung-chieh Shan. 2008. Lightweight Monadic Regions. In Proceedings of the First ACM SIGPLAN Symposium on Haskell (Haskell ’08) . ACM, New York, NY, USA, 1–12.

Digital Library

[20]

John Launchbury. 1993. A Natural Semantics for Lazy Evaluation. In POPL. 144–154.

Digital Library

[21]

John Launchbury and Simon L. Peyton Jones. 1995. State in Haskell. LISP and Symbolic Computation 8, 4 (1995), 293–341.

Digital Library

[22]

Ben Lippmeier, Fil Mackay, and Amos Robinson. 2016. Polarized data parallel data flow. In Proceedings of the 5th International Workshop on Functional High-Performance Computing . ACM, 52–57.

Digital Library

[23]

Nicholas D. Matsakis and Felix S. Klock, II. 2014. The Rust Language. Ada Lett. 34, 3 (Oct. 2014), 103–104.

Digital Library

[24]

Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic. 2010. Lightweight linear types in system f. In Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation . ACM, 77–88.

Digital Library

[25]

Conor McBride. 2016. I Got Plenty o’ Nuttin’. Springer International Publishing, Cham, 207–233.

[26]

J. Garrett Morris. 2016. The best of both worlds: linear functional programming without compromise. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016 . 448–461.

Digital Library

[27]

Bryan O’Sullivan. 2013. The Criterion benchmarking library. http://github.com/bos/criterion

[28]

Tomas Petricek, Dominic Orchard, and Alan Mycroft. 2013. Coeffects: Unified Static Analysis of Context-Dependence. Springer Berlin Heidelberg, Berlin, Heidelberg, 385–397.

Digital Library

[29]

François Pottier. 1998. Type Inference in the Presence of Subtyping: from Theory to Practice. Research Report RR-3483. INRIA. https://hal.inria.fr/inria-00073205

[30]

Ilya Sergey, Dimitrios Vytiniotis, and Simon Peyton Jones. 2014. Modular, Higher-order Cardinality Analysis in Theory and Practice. SIGPLAN Not. 49, 1 (Jan. 2014), 335–347.

Digital Library

[31]

Robert E Strom. 1983. Mechanisms for compile-time enforcement of security. In Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages . ACM, 276–284.

Digital Library

[32]

Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. 2007. System F with Type Equality Coercions. In Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI ’07) . ACM, New York, NY, USA, 53–66.

Digital Library

[33]

Jesse A Tov and Riccardo Pucella. 2011. Practical affine types. In POPL. ACM, 447–458.

[34]

Michael Vollmer, Sarah Spall, Buddhika Chamith, Laith Sakka, Chaitanya Koparkar, Milind Kulkarni, Sam Tobin-Hochstadt, and Ryan R. Newton. 2017. Compiling Tree Transforms to Operate on Packed Representations. In 31st European Conference on Object-Oriented Programming (ECOOP 2017) (Leibniz International Proceedings in Informatics (LIPIcs)), Peter Müller (Ed.), Vol. 74. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 26:1–26:29.

[35]

Philip Wadler. 1990. Linear types can change the world. In Programming Concepts and Methods, M Broy and C B Jones (Eds.). North-Holland.

[36]

Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg. 2017. A Specification for Dependent Types in Haskell. Proc. ACM Program. Lang. 1, ICFP, Article 31 (Aug. 2017), 29 pages.

Digital Library

[37]

Dengping Zhu and Hongwei Xi. 2005. Safe Programming with Pointers Through Stateful Views. Springer Berlin Heidelberg, Berlin, Heidelberg, 83–97.

Digital Library

Cited By

Ângelo PIgarashi AT. Vasconcelos V(2024)Linear Contextual Metaprogramming and Session TypesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.401.1401(1-10)Online publication date: 6-Apr-2024
https://doi.org/10.4204/EPTCS.401.1
Saffrich HNishida YThiemann P(2024)Law and Order for Typestate with BorrowingProceedings of the ACM on Programming Languages10.1145/36897638:OOPSLA2(1475-1503)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689763
Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Show More Cited By

Index Terms

Linear Haskell: practical linearity in a higher-order polymorphic language
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
    2. General programming languages
      1. Language features
      2. Language types
        Functional languages

Recommendations

Linearly qualified types: generic inference for capabilities and uniqueness

A linear parameter must be consumed exactly once in the body of its function. When declaring resources such as file handles and manually managed memory as linear arguments, a linear type system can verify that these resources are used safely. However, ...
Polymorphic variants in Haskell
Haskell '06: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell

In languages that support polymorphic variants, a single variant value can be passed to many contexts that accept different sets of constructors. Polymorphic variants can be used in order to introduce extensible algebraic datatypes into functional ...
Practical affine types
POPL '11

Alms is a general-purpose programming language that supports practical affine types. To offer the expressiveness of Girard's linear logic while keeping the type system light and convenient, Alms uses expressive kinds that minimize notation while ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue POPL

January 2018

1961 pages

EISSN:2475-1421

DOI:10.1145/3177123

Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 December 2017

Published in PACMPL Volume 2, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Evaluated & Functional

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

78
Total Citations
View Citations
2,562
Total Downloads

Downloads (Last 12 months)431
Downloads (Last 6 weeks)65

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ângelo PIgarashi AT. Vasconcelos V(2024)Linear Contextual Metaprogramming and Session TypesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.401.1401(1-10)Online publication date: 6-Apr-2024
https://doi.org/10.4204/EPTCS.401.1
Saffrich HNishida YThiemann P(2024)Law and Order for Typestate with BorrowingProceedings of the ACM on Programming Languages10.1145/36897638:OOPSLA2(1475-1503)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689763
Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Lobo-Vesga ERusso AGaboardi MCortiñas C(2024)Sensitivity by ParametricityProceedings of the ACM on Programming Languages10.1145/36897268:OOPSLA2(415-441)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689726
Giannini PDuso GDi Stefano L(2024)Coeffects for MiniJava: Cf-MjProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686232(30-36)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686232
Lorenzen AWhite LDolan SEisenberg RLindley S(2024)Oxidizing OCaml with Modal Memory ManagementProceedings of the ACM on Programming Languages10.1145/36746428:ICFP(485-514)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674642
Marshall DOrchard D(2024)Functional Ownership through Fractional UniquenessProceedings of the ACM on Programming Languages10.1145/36498488:OOPSLA1(1040-1070)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649848
Tang WHillerström DLindley SMorris J(2024)Soundly Handling LinearityProceedings of the ACM on Programming Languages10.1145/36328968:POPL(1600-1628)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632896
Smeding TVákár M(2024)Efficient CHADProceedings of the ACM on Programming Languages10.1145/36328788:POPL(1060-1088)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632878
Chen RSander I(2024)A Quantitative Type Approach to Formal Component-Based System Design2024 Forum on Specification & Design Languages (FDL)10.1109/FDL63219.2024.10673844(1-10)Online publication date: 4-Sep-2024
https://doi.org/10.1109/FDL63219.2024.10673844
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents