data types and initiality

To: types@theory.LCS.MIT.EDU
Subject: data types and initiality
From: tobias@dash2.lcs.mit.edu (Tobias Nipkow)
Date: Wed, 9 Nov 88 20:49:08 EST
Sender: meyer@theory.LCS.MIT.EDU

Date: Wed, 9 Nov 88 19:34:15 EST
Cc: dts%cstvax.ed.ac.uk%NSS.Cs.Ucl.AC.UK@CAF.MIT.EDU

This debate about what constitutes a "correct" implementation of a data type
has been going on for some time. The world seems to be divided into those
people who think the initial spec algebra should be some homomorphic image of
the implementation, and those that opt for an observational equivalence
definition. Then the question arises what the observations are. I have always
supported the observational point of view, and in particular using programs
as observers. But many people think that it makes sense to be more
restrictive than that, e.g. by enforcing homomorphic relationships. It is
usually argued that for some reason it is useful to give the specifier
stronger control of the possible implementations. I have never been convinced
and believe the homomorphic image definition is a historic accident.

In sumary: no, you are not attacking a straw man, and people in the
(abstract) data types community should be more aware of things like
representation independence theorems for the lambda-calculus.

Re Ehrig and Mahr: Unless you are referring to their second book (is it out
yet?), I don't think they claim that implementations should be isomorphic to
the initial spec algebra - they don't discuss implementations at all.

Tobias Nipkow