Jean-Philippe Bernardy
Simon Peyton Jones
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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
- 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. Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- Jean-Marc Andreoli. 1992. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2, 3 (1992), 297–347. Google ScholarCross Ref
- Robert Atkey. 2017. The Syntax and Semantics of Quantitative Type Theory. (2017). Under submission.Google Scholar
- 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.Google ScholarCross Ref
- 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.09756Google Scholar
- 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 .Google Scholar
- Mathieu Boespflug, Facundo Dominguez, Alexander Vershilov, and Allen Brown. 2014. Project H: Programming R in Haskell. (2014). Talk at IFL 2014.Google Scholar
- Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program. 23, 5 (2013), 552–593. Google ScholarCross Ref
- Edwin Brady. 2017. Type-driven Development of Concurrent Communicating Systems. Computer Science 18, 3 (2017). https://journals.agh.edu.pl/csci/article/view/1413 Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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.htmlGoogle Scholar
- Evan Czaplicki. 2012. Elm: Concurrent FRP for functional guis. Senior thesis. Harvard University.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science 50, 1 (1987), 1–101. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- John Launchbury. 1993. A Natural Semantics for Lazy Evaluation. In POPL. 144–154. Google ScholarDigital Library
- John Launchbury and Simon L. Peyton Jones. 1995. State in Haskell. LISP and Symbolic Computation 8, 4 (1995), 293–341. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Nicholas D. Matsakis and Felix S. Klock, II. 2014. The Rust Language. Ada Lett. 34, 3 (Oct. 2014), 103–104. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Conor McBride. 2016. I Got Plenty o’ Nuttin’. Springer International Publishing, Cham, 207–233. Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Bryan O’Sullivan. 2013. The Criterion benchmarking library. http://github.com/bos/criterionGoogle Scholar
- Tomas Petricek, Dominic Orchard, and Alan Mycroft. 2013. Coeffects: Unified Static Analysis of Context-Dependence. Springer Berlin Heidelberg, Berlin, Heidelberg, 385–397. Google ScholarDigital Library
- 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-00073205Google Scholar
- 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. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Jesse A Tov and Riccardo Pucella. 2011. Practical affine types. In POPL. ACM, 447–458.Google Scholar
- 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. Google ScholarCross Ref
- Philip Wadler. 1990. Linear types can change the world. In Programming Concepts and Methods, M Broy and C B Jones (Eds.). North-Holland.Google Scholar
- 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. Google ScholarDigital Library
- Dengping Zhu and Hongwei Xi. 2005. Safe Programming with Pointers Through Stateful Views. Springer Berlin Heidelberg, Berlin, Heidelberg, 83–97. Google ScholarDigital Library
Index Terms
- Linear Haskell: practical linearity in a higher-order polymorphic language
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 HaskellIn 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 '11Alms 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