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

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ć'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.

A prototype writen in Haskell can be found at http://diaz-caro.web.unq.edu.ar/IsoAsEq-v1.0.tar.gz

References in corpus (3)

• Non-idempotent intersection types and strong normalisation
• Bounding normalization time through intersection types
• Call-by-value non-determinism in a linear logic type discipline

Cited by in corpus (2)

• The exp-log normal form of types
• A Quick Overview on the Quantum Control Approach to the Lambda Calculus