Applicative Notions in ML-like Programs
Budi H Ling · ERA · 1998
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