Edison RC3

[Robert Dockins]

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
> 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