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

DÍAZ-CARO, ALEJANDRO; MARTÍNEZ LÓPEZ, PABLO E.

ACM International Conference Proceeding Series

Association for Computing Machinery

Lugar: Nueva York; Año: 2015 vol. IFL p. 1 - 15

We propose an implementation of λ+, a recently introduced simply typed lambda-calculus with pairs where isomorphic types are made equal. The rewrite system of λ+ is a rewrite system modulo an equivalence relation, which makes its implementation non-trivial. We also extend λ+ with natural numbers and general recursion and use Bekić´s theorem to split mutual recursions. This splitting, together with the features of λ+, 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.