Introduction

Consider the following statements:

• A programming language type is only a set of values.
• A type constructor is an expression resulting in a set of values.
• Operators such as $+$ and $-$ are functions and do not form part of types.
• Expressions are function applications, and the type of an expression is the set of values representing the co-domain of the last function to be applied.
• A programming language variable is a functional mapping from the empty set to the set of values making up the type of the variable.
• An assignment statement partially redefines the rule according to which a variable maps the empty set to its type set.

From these statements, a formal model of the semantics of types, variables, assignments and expressions can be constructed. In the rest of this paper, this model will be referred to as the functional data model.

There are many other mathematical formalisms that can be used to model variables and types, but none are as simple and intuitive as the functional data model. Of course, since the functional model is so simple, it does not model all aspects of the type systems of typical programming languages. For example, the functional data model does not associate types with representations or with sets of operators. As a consequence, language theorists tend to explore more complicated formalisms.

Some of the more complicated formalisms used to model old programming languages are in turn used as the basis for designing new programming languages, which tend to be more consistent and complete than designs not based on some formalism. The lambda calculus has been a popular choice.

Given the simplicity and intuitive appeal of the functional data model, it is worth asking whether the functional model can profitably be used as the basis for designing a programming language which is consistent, complete and expressive. Earlier work by Shipman[6] and Buneman[1] already goes a long way towards proving that this can be done. However, the functional data model has not yet been used as a basis for designing an imperative language in the Algol tradition. The author is currently designing such a language, and the type system of the preliminary version of this language is presented in this paper.