Edison RC3

[Nils Anders Danielsson]

On Wed, 05 Apr 2006, Robert Dockins <robdockins at fastmail.fm> wrote:

> The 3rd release candidate for Edison 1.2 is now avaliable.

In the documentation you write:

  An instance of an abstract data type is considered indistinguishable
  from another if all possible applications of unambiguous operations
  to both yield indistinguishable results. In this context, we
  consider bottom to be distinguishable from non-bottom results, and
  indistinguishable from other bottom results.

I believe this wording is somewhat too strong. It is usually very hard
to achieve what you are claiming above, since (among other things)
bottom and const bottom are distinguishable.

Typically when Haskellers claim various properties for their functions
they ignore bottoms (and often also infinite values), reasoning in a
"fast and loose" way. This is seldom explicitly mentioned, though, so
I guess many may not be aware of this. Your statement makes it seem as
if you have done more than the ordinary, fast and loose, reasoning,
and I find it misleading.

Of course, if you have actually gone to the trouble of verifying your
statement for all the data structures, then you should keep the
statement (with an extra note about proofs written or tests
performed).

-- 
/NAD