On Wed, 05 Apr 2006, Robert Dockins
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