A Semantic framework for deterministic functional input/output

Abstract

This dissertation presents a pure functional language called Curio. This language is unusual in possessing a rigorous yet general semantics for I/O which permits both formal proofs and a fine-tuned approach to concurrency. This is achieved by describing the language semantics in terms of an abstract model of the I/O application programmer interface (API). We begin by introducing this model, which simulates how the API affects some global world state and describes the extent to which certain I/O actions are order independent. We then introduce Curio, which extends a pure functional language with five primitives for monadic I/O and explicit concurrency. Each process is at runtime associated with what we call an "I/O context" and this outlines the I/O actions that the process is allowed to perform. The language's semantics are given in terms of a simple implementation in the metalanguage, Core-Clean. It is proved formally that if an I/O model obeys some broad properties then, despite concurrency, program execution is always deterministic. This result is made more substantial by the fact that concurrent processes may communicate with one another via the API. We then show how a large fragment of Haskell 98's I/O interface can be modelled in Curio. To do this we found it necessary to develop API combinators which allow larger APIs to be constructed from smaller ones in a way that preserves deterministic behaviour. It was also necessary to solve the technical problem of how two processes may allocate data locally within a single global state. We present some example applications which demonstrate how Curio appears to lead to more expressive, powerful I/O code compared to that of existing approaches.