LFPL is a functional language for non-size increasing computation with an operational semantics that allows in-place update. The semantics is correct for all well-typed programs thanks to linear restrictions on the typing. Nevertheless, the linear typing is very strict and rejects many correct, natural in-place update algorithms.
We investigate a general approach to easing the tight linear restrictions of LFPL by generalising the static analysis used by Aspinall & Hofmann [2002]. It consists in devising new type systems for the core language of LFPL whose judgements express sets of rely-guarantee pairs with assertions about the operational semantics, namely about the heap representation of the arguments and the result. The method can be applied to other functional languages with heap based operational semantics.
As an example and application of the approach we reformulate the language of Aspinall & Hofmann [2002] from this perspective and prove the correctness of some of its crucial typing rules, show its type inference algorithm and the existence of principal types relative to the simple LFPL typing. We refer to other languages based on LFPL which fit into the approach.
repository in informatics.ed.ac.uk, BibTeX, pdf(a4, colours), ps.gz(a4, colours). ps.gz(a4, b&w).