RAIRO - Theoretical Informatics and Applications

Research Article

Final Dialgebras: From Categories to Allegories

Roland Backhousea1 and Paul Hoogendijka2

a1 School of Computer Science and IT, University of Nottingham, Nottingham NG8 1BB, U.K.

a2 Philips Research Laboratories, Prof. Holstlaan 4, 5656 AA Eindhoven, The Netherlands.

Abstract

The study of inductive and coinductive types (like finite lists and streams, respectively) is usually conducted within the framework of category theory, which to all intents and purposes is a theory of sets and functions between sets. Allegory theory, an extension of category theory due to Freyd, is better suited to modelling relations between sets as opposed to functions between sets. The question thus arises of how to extend the standard categorical results on the existence of final objects in categories (for example, coalgebras and products) to their existence in allegories. The motivation is to streamline current work on generic programming, in which the use of a relational theory rather than a functional theory has proved to be desirable. In this paper, we define the notion of a relational final dialgebra and prove, for an important class of dialgebras, that a relational final dialgebra exists in an allegory if and only if a final dialgebra exists in the underlying category of maps. Instances subsumed by the class we consider include coalgebras and products. An important lemma expresses bisimulations in allegorical terms and proves this equivalent to Aczel and Mendler's categorical definition.

(Received October 27 1998)

(Revised April 29 1999)

(Online publication August 15 2002)

Key Words:

  • Programming theory;
  • theory of datatypes;
  • inductive type;
  • co-inductive type;
  • relation algebra;
  • category theory;
  • allegory theory;
  • generic programming;
  • polytypic programming.

Mathematics Subject Classification:

  • 68N05
Metrics