The formal description of data types using sketches

Abstract

This paper is an exposition of the basic ideas of the mathematical theory of sketches and a detailed description of some of the ways in which this theory can be used in theoretical computer science to specify datatypes. In particular, this theory provides a convenient way of introducing datatypes which have variants, for example in case of errors or nil pointers. The semantics is a generalization of initial algebra semantics which in some cases allows initial algebras depending on a parameter such as a bound for overflow.