Re: Edison RC3

5 Apr 2006


      On Apr 5, 2006, at 5:12 AM, Nils Anders Danielsson wrote:
...
On Wed, 05 Apr 2006, Robert Dockins  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
performed).
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.
...
-- 
/NAD
Thanks for pointing that out (and for letting me know that at least  
one person out there reads the documentation! ;-)   )


Rob Dockins

Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
           -- TMBG