LFPL with Types for Deep Sharing

Abstract

First-order 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 welltyped programs thanks to linear restrictions on the typing. Nevertheless, the linear typing is very strict and rejects many correct, natural in-place update algorithms. Aspinall and Hofmann added usage aspects to variables in LFPL terms in order to typecheck more programs while keeping correctness.

We further extend this language to typecheck even more programs, especially those that use data sharing on the heap. We do it by assigning usage aspects to certain type subterms instead of whole types thus referring to value portions instead of the whole values. The usage aspects express preconditions of separation between certain argument portions, the guarantees of preservation of certain argument portions and containment of every result portion in some set of argument portions and a rely-precondition for every separation guarantee within the result value. The new typing allows deterministic type-checking with automatic synthesis of the best usage aspects for recursively defined functions.