Precise Typing of Abstract Data Type Specifications

Abstract

There are two important notions of types being used in programming languages today. In the concept called types, types are algebras; the semantics of programs is described in terms of operations in these algebras. Another notion of found in most of the typed programming languages in actual use regards types as sets of objects; the elements of types are the objects manipulated by the operators of a programming language. I shall be careful to use abstract when I mean the algebraic notion, and data or simply type to mean the set-based concept.This paper presents a formal theory of types as an approximation to the exact semantics of a language, following the lead of Milner [Mil78]. The semantics is based upon multi-sorted algebras [ADJ73, 76, 77, 78] and is applied to a language consisting of equational specifications that define an type. The principal results of the paper are to characterize a class of typings as uniform approximations to an exact semantics, to extend Milner's theory of types to include types formed by coproduct construction, and to explicate typing as an (approximate) semantics for an equational theory.In developing a formal theory of types as multi-sorted algebras, the word is used to designate names used to distinguish various sets of objects that may constitute the domains of operators. Sorts are thus analogous to types in programming languages. However, the sort signatures given to operators of types do not themselves constitute a very richly descriptive language. Sort names can be formed into sequences, corresponding to product construction in an object domain, but the theory (multi-sorted Σ-algebras) does not seem to allow alternation sequences of sorts, corresponding to coproduct construction in an object domain. If this were possible, then sort signatures could actually fulfill the role of types. We shall see that alternation sequences in signatures arise naturally as a consequence of the semantics given to an equational theory.