Call-by-name extensionality and confluence. (27th February 2017)

• Record Type: Journal Article
• Authors: JOHNSON-FREYD, PHILIP; DOWNEN, PAUL; ARIOLA, ZENA M.
• Is Part Of: Journal of functional programming. Volume 27(2017)
• Publication Date: 2017-02-27
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S095679681700003X
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: Designing rewriting systems that respect functional extensionality for call-by-name languages with effects turns out to be surprisingly challenging. Simply interpreting extensional laws like η as reduction rules easily breaks confluence. We explore these issues in the setting of a sequent calculus. Building on an insight that appears in different aspects of the theory of call-by-name functional languages—confluent rewriting for two independent control calculi and sound continuation-passing style transformations—we give a confluent reduction system for lazy extensional functions. Finally, we consider limitations to this approach when used for strict evaluation and types beyond functions.