[Prev][Next][Index][Thread]
data types and initiality
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