The Best of Both Worlds: Linear Functional Programming without Compromise

J. Garrett Morris

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present a linear functional calculus with both the safety guarantees expressible with linear types and the rich language of combinators and composition provided by functional programming. Unlike previous combinations of linear typing and functional programming, we compromise neither the linear side (for example, our linear values are first-class citizens of the language) nor the functional side (for example, we do not require duplicate definitions of compositions for linear and unrestricted functions). To do so, we must generalize abstraction and application to encompass both linear and unrestricted functions. We capture the typing of the generalized constructs with a novel use of qualified types. Our system maintains the metatheoretic properties of the theory of qualified types, including principal types and decidable type inference. Finally, we give a formal basis for our claims of expressiveness, by showing that evaluation respects linearity, and that our language is a conservative extension of existing functional calculi.
Original languageEnglish
Title of host publicationICFP 2016 Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
Place of PublicationNara, Japan
PublisherACM
Pages448-461
Number of pages14
ISBN (Electronic)978-1-4503-4219-3
DOIs
Publication statusPublished - 4 Sep 2016
Event21st ACM SIGPLAN International Conference on Functional Programming - Nara, Japan
Duration: 18 Sep 201624 Sep 2016
https://conf.researchr.org/home/icfp-2016

Publication series

NameACM SIGPLAN Notices
PublisherACM
Number9
Volume51
ISSN (Print)0362-1340
ISSN (Electronic)1558-1160

Conference

Conference21st ACM SIGPLAN International Conference on Functional Programming
Abbreviated titleICFP 2016
CountryJapan
CityNara
Period18/09/1624/09/16
Internet address

Fingerprint

Dive into the research topics of 'The Best of Both Worlds: Linear Functional Programming without Compromise'. Together they form a unique fingerprint.

Cite this