Final algebra semantics and data type extensions

摘要

We consider the problem of data type extensions. Guttag, Horowitz, and Musser have pointed out that in this situation the naive initial algebra approach requires the data type to save too much information. We formulate a category of implementations of such an extension, and we show that such a category has a final object. The resulting semantics is closer to that of Hoare, since it can be argued that an abstract data type in the sense of Hoare is a final object in the category of representations of that type. We consider as an example the specification of integer arrays, and we show that our specification yields arrays as its abstract data type. The connection with initial algebra semantics is discussed.