Showing 1–2 of 2 results for author: López, P E M

Polymorphic System I

Authors: Cristian F. Sottile, Alejandro Díaz-Caro, Pablo E. Martínez López

Abstract: System I is a simply-typed lambda calculus with pairs, extended with an equational theory obtained from considering the type isomorphisms as equalities. In this work we propose an extension of System I to polymorphic types, adding the corresponding isomorphisms. We provide non-standard proofs of subject reduction and strong normalisation, extending those of System I. System I is a simply-typed lambda calculus with pairs, extended with an equational theory obtained from considering the type isomorphisms as equalities. In this work we propose an extension of System I to polymorphic types, adding the corresponding isomorphisms. We provide non-standard proofs of subject reduction and strong normalisation, extending those of System I. △ Less

Submitted 19 May, 2021; v1 submitted 8 January, 2021; originally announced January 2021.

Comments: 20 pages plus appendix

Journal ref: In IFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages (IFL 2020). Association for Computing Machinery, New York, NY, USA, 127-137

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

Authors: Alejandro Díaz-Caro, Pablo E. Martínez López

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… ▽ More 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. △ Less

Submitted 11 February, 2016; v1 submitted 30 November, 2015; originally announced November 2015.

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

ACM Class: F.4.1

Journal ref: ACM Proceedings of IFL'15(9), 2015