Efficiency of lambda-encodings in total type theory. (10th March 2016)

• Record Type: Journal Article
• Authors: STUMP, AARON; FU, PENG
• Is Part Of: Journal of functional programming. Volume 26(2016)
• Publication Date: 2016-03-10
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796816000034
• Languages: English
• ISSNs: 0956-7968

Abstract

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.