[Haskell-cafe] Class invariants/laws

[Janis Voigtlaender]

ajb at spamcop.net wrote:
>> Yes. But actually what we would need would be that it checks as well
>> that we have implemented at *most* a minimal set of operations.
>> Otherwise, we are back to the point where I can implement both (==) and
>> (/=), and in a way that the supposed invariant is broken.
> 
> 
> Except that there are many circumstances where I can write an operation
> that's more efficient (or more lazy, or whatever) than the default, even
> though they do the same thing.

Yes, that's the standard motivation for allowing to implement more of
the class methods than would actually be needed. But the "(or more lazy,
or whatever)"-part bodes ill. If I understand correctly what you mean by
"more lazy", it implies that you are willing to accept variations of
complementary methods like (==) and (/=) that do satisfy the expected
invariant, except for their behaviour with respect to partially defined
inputs. But exactly this "up to bottom"-reasoning is what gets us into
trouble with free theorems in Haskell. If you look at the
class-respectance conditions generated for the language subset including
selective strictness, you will find preconditions related to _|_. So it
is dangerous to do both:

1. record only a subset of those restrictions based on the argument that
the methods are anyway tied together via invariants

2. require those same invariants to hold "up to _|_" only

The result would be free theorems that might be wrong for class
instances that satisy the invariants suggested by default method
implementations only in this lax way.

Better, then, to go the full way and record the restrictions for all
class methods, thus being prepared for *any* instance definition, be it
fully compliant with the default method implementation, only laxly
compliant, or not at all.

Ciao, Janis.

-- 
Dr. Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt at tcs.inf.tu-dresden.de