The best of both worlds: linear functional programming without compromise

DOI10.1145/2951913.2951925MaRDI QIDQ2985794zbMATH OpenOpenAlexFDO

Authors J. Garrett Morris

Publication date 10 May 2017

Published in Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1612.06633

zbMATH Keywords

linear typesqualified typessubstructural types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

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.

Recommendations

• Enriching an Effect Calculus with Linear Types
• On regions and linear types (extended abstract)
• A type system for bounded space and functional in-place update
• scientific article; zbMATH DE number 1223626
• Lilac: a functional programming language based on linear logic

Cited in

(6)

• FabULous interoperability for ML and a linear language
• Enriching an Effect Calculus with Linear Types
• LNL-FPC: the linear/non-linear fixpoint calculus
• Modular inference of linear types for multiplicity-annotated arrows
• Linearity and uniqueness: an entente cordiale
• Kind inference for the \textsc{FreeST} programming language

This page was built for publication: The best of both worlds: linear functional programming without compromise

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2985794)