Isomorphisms considered as equalities: Projecting functions and enhancing partial application through and implementation of lambda+

TL;DR

This paper presents an implementation of lambda+ that treats isomorphic types as equal, enabling advanced program transformations like projection and enhanced partial application through a rewrite system modulo type equivalence.

Contribution

It introduces a novel implementation of lambda+ with type isomorphism handling, extending it with natural numbers, recursion, and a new approach to program transformation.

Findings

Implementation of lambda+ with type isomorphism as equality.

Extension of lambda+ with natural numbers and recursion.

New program transformation techniques using projection and partial application.

Abstract

We propose an implementation of lambda+, a recently introduced simply typed lambda-calculus with pairs where isomorphic types are made equal. The rewrite system of lambda+ is a rewrite system modulo an equivalence relation, which makes its implementation non-trivial. We also extend lambda+ with natural numbers and general recursion and use Beki\'c's theorem to split mutual recursions. This splitting, together with the features of lambda+, allows for a novel way of program transformation by reduction, by projecting a function before it is applied in order to simplify it. Also, currying together with the associativity and commutativity of pairs gives an enhanced form of partial application.