Conference proceeding
The best of both worlds: linear functional programming without compromise
Proceedings of the 21st ACM SIGPLAN International Conference on functional programming, Vol.51(9), pp.448-461
ICFP 2016
09/04/2016
DOI: 10.1145/2951913.2951925
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.
Details
- Title: Subtitle
- The best of both worlds: linear functional programming without compromise
- Creators
- J. Garrett Morris - University of Edinburgh
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings of the 21st ACM SIGPLAN International Conference on functional programming, Vol.51(9), pp.448-461
- Series
- ICFP 2016
- DOI
- 10.1145/2951913.2951925
- ISSN
- 1523-2867
- Publisher
- ACM
- Grant note
- DOI: 10.13039/501100000266, name: Engineering and Physical Sciences Research Council, award: EP/K034413/1
- Language
- English
- Date published
- 09/04/2016
- Academic Unit
- Computer Science
- Record Identifier
- 9984259418702771
Metrics
6 Record Views