Incrementality and effect simulation in the simply typed lambda calculus
Lourdes del Carmen González Huesca · 2015
Certified programming is a framework in which any program is correct by construction. Proof assistants and dependently typed programming languages are the representatives of this paradigm where the proof and implementation of a program are done at the same time. However, it has some limitations: a program in Type Theory is built only with pure and total functions. Our objective is to write efficient and certified programs. The contributions of this work are the formalization, in the Simply Typed Lambda Calculus, of two mechanisms to achieve efficiency: to validate impure computations and to optimize computations by incrementality. An impure computation, that is a program with effects, and its validation in a functional and total language is done through a posteriori simulation. The simulation is performed afterwards on a monadic procedure and is guided by a prophecy. An efficient oracle is responsible for producing prophecies which is actually, the monadic procedure itself translated into an effectful programming language. The second contribution is an optimization to perform incremental computations. Incrementality as a way to propagate an input change into a corresponding output change is guided by formal change descriptions over terms and dynamic differentiation of functions. Displaceable types represent data-changes while an extension of the simply typed lambda calculus with differentials and partial derivatives offers a language to reason about incrementality.