Applicative Notions in ML-like Programs

Budi Halim Ling

Abstract:

Pure functional languages are expressive tools for writing modular and reliable code. State in programming languages is a useful tool for programming dynamic systems. However, their combination yields programming languages that are difficult to model and to reason about.

There have been ongoing attempts to find subsets of the whole languages which have good properties; in particular subsets where the programs are more modular and the side effects are controlled. The existing studies are: interference control, typing with side-effects information, and linear logic based languages. This thesis presents a new classification for a paradigm called constant program throughout a computational invariant. A program is called constant throughout an invariant R if its input-output behaviour is constant over any variations of state that satisfy the invariant R. Hence such a program behaves in an applicative way when it is executed in a context that satisfies the invariant R.

The language of discussion is a pure ML fragment augmented with ref, :=, and !. Programs with side effects are modelled in terms of sets, functions, and the side effect monad. Computational invariants are modelled in terms of transition systems. The notion of being constant throughout an invariant requires the notion of indistinguishability throughout an invariant and we define the latter using logical relation technique. We give two definitions of each of them: the first one can be used for reasoning about programs with at stores adequately. The second one is more sensitive to the behaviour of ref and gives a better account of constant programs with dynamic allocations.

Our results are: indistinguishability throughout an invariant R is an equivalence relation over elements that are constant throughout R, and the notion of being constant throughout an invariant is preserved under function application. On the practical side we present some substantial ML examples which use references and side effects but externally behave in a constant way, together with the proofs that they are classified as being constant. These are evidences that our notions are useful concepts in the practise of writing modular programs.

ECS-LFCS-98-390. This is a 131-page M.Phil thesis. It is available in the following forms.

This report is available in the following formats:

Previous | Index | Next