Logic of fusion

TL;DR

This paper explores the logical foundations of program fusion, particularly deforestation, through the Curry-Howard isomorphism, offering a new interpretation of parametricity and transformations in functional programming.

Contribution

It provides a novel logical analysis of build fusion over various datatypes, extending the Curry-Howard correspondence to program optimization techniques.

Findings

Logical interpretation of parametricity via paranatural transformations

Extension of fusion analysis to inductive and coinductive datatypes

Connection between program fusion and cut elimination in logic

Abstract

The starting point of this work is the observation that the Curry-Howard isomorphism, relating types and propositions, programs and proofs, composition and cut, extends to the correspondence of program fusion and cut elimination. This simple idea suggests logical interpretations of some of the basic methods of generic and transformational programming. In the present paper, we provide a logical analysis of the general form of build fusion, also known as deforestation, over the inductive and the coinductive datatypes, regular or nested. The analysis is based on a novel logical interpretation of parametricity in terms of the paranatural transformations, introduced in the paper.