robdockins at fastmail.fm
Wed Apr 5 11:01:32 EDT 2006
On Apr 5, 2006, at 5:12 AM, Nils Anders Danielsson wrote:
> 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.
Ugh! Of course, you are right (eta-conversion bites again!). Most of
this paragraph is left-over from when I was using the terms
'ambiguous' vs 'well-defined' rather than 'ambiguous' vs
'unambiguous'. I felt that I needed to say that 'well-defined' !=
'not bottom', and that meant I had to talk about bottom. Now, I'm
using 'unambiguous' which doesn't have that particular confusion, I
should probably rewrite that paragraph.
> 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.
So you think it would be clearer if I just ignored bottom as well?
That's certainly easier on me; it means people can't start providing
nasty counterexamples to my function contracts using 'seq'!
> 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
No, this has not been done. I have thought about employing
Programmatica to formalize the contracts and verify implementations,
but its just a pipe-dream for now.
Thanks for pointing that out (and for letting me know that at least
one person out there reads the documentation! ;-) )
Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
More information about the Libraries