Journal article
Efficiency of lambda-encodings in total type theory
Journal of functional programming, Vol.26, pp.1-31
2016
DOI: 10.1017/S0956796816000034
Abstract
This paper proposes a new typed lambda-encoding for inductive types which, for Peano numerals, has the expected time complexities for basic operations like addition and multiplication, has a constant-time predecessor function, and requires only quadratic space to encode a numeral. This improves on the exponential space required by the Parigot encoding. Like the Parigot encoding, the new encoding is typable in System F-omega plus positive-recursive type definitions, a total type theory. The new encoding is compared with previous ones through a significant case study: mergesort using Braun trees. The practical runtime efficiency of the new encoding, and the Church and Parigot encodings, are compared by two translations, one to Racket and one to Haskell, on a small suite of benchmarks.
Details
- Title: Subtitle
- Efficiency of lambda-encodings in total type theory
- Creators
- AARON Stump - University of IowaPENG FU - University of Dundee
- Resource Type
- Journal article
- Publication Details
- Journal of functional programming, Vol.26, pp.1-31
- Publisher
- Cambridge University Press
- DOI
- 10.1017/S0956796816000034
- ISSN
- 0956-7968
- eISSN
- 1469-7653
- Number of pages
- 31
- Language
- English
- Date published
- 2016
- Academic Unit
- Computer Science
- Record Identifier
- 9984259408302771
Metrics
4 Record Views