data types and initiality

To: types@theory.LCS.MIT.EDU
Subject: data types and initiality
From: John Mitchell <jcm@ra.stanford.edu>
Date: Wed, 9 Nov 88 17:46:55 EST
Sender: meyer@theory.LCS.MIT.EDU

Date: Wed, 9 Nov 88 10:27:32 PDT
Cc: bhoward@polya.lcs.mit.edu, eswolf@polya.lcs.mit.edu

In preparing a lecture about algebraic data types,
I came across the claim (in several places, including the
book by Ehrig and Mahr) that a "correct" implementation
of a specification is any algebra that is isomorphic
to the initial algebra. While I am willing to believe that
the initial algebra is OK, this seems unreasonably
restrictive. I would propose, at the very least,
that anything observably equivalent to the initial
algebra is OK. In fact, this seems like a reasonable
definition of acceptable, since one could claim that
proofs by induction are sound (in some suitable sense)
even for these non-initial algebras, and should
fail otherwise. 

Does anyone want to argue in favor of this "standard"
point of view? Do you know anyone else who really 
believes this, or am I just attacking a straw man?

John Mitchell