Projective ML
It is shown that projective ML possesses the subject reduction property, which means that well-typed programs can be reduced safely and is built on by adding the ML Let typing rule to the simply typed projective calculus.
Abstract
We propose a projective lambda calculus as the basis for operations on records. Projections operate on elevations, that is, records with defaults. This calculus extends lambda calculus while keeping its essential properties. We build projective ML from this calculus by adding the ML Let typing rule to the simply typed projective calculus. We show that projective ML possesses the subject reduction property, which means that well-typed programs can be reduced safely. Elevations are practical data structures that can be compiled efficiently. Moreover, standard records are difinable in terms of projections.