[Haskell-cafe] Re: [Haskell] Announce: generating free theorems, online and offline

[Dan Weston]

 > Now that I look at it, the report notes that:
 >
 >     -- Note that (min x y, max x y) = (x,y) or (y,x)
 >
 > but never says that this requirement is mandatory.

That's because the comment applies only to the default implementation, 
not in general.

The report does require that "The Ord class is used for totally ordered 
datatypes." If the type is a e.g. a set of equivalence classes (say a 
tuple of integers to represent rationals), then there is a well-defined 
total ordering. A min or max function is free to return any valid 
representation of the rational, which may differ from either of the 
arguments, so long as the difference is not observable by functions in 
Ord or any superclass of Ord.

ajb at spamcop.net wrote:
> G'day all.
> 
> Quoting Janis Voigtlaender <voigt at tcs.inf.tu-dresden.de>:
> 
>> Okay, it is quite natural to take this stand. But as you say, there is
>> no such commitment in the language definition. And even if there were, I
>> doubt it would be possible to enforce such invariants in a compiler. So
>> there would be "illegal" programs that are nevertheless accepted by the
>> compilers. Not what we want, do we, in Haskell land?
> 
> I guess this is, at its core, a philosophical question:  Does the
> existence of default implementations imply that any specialised
> implementation must do the same thing (modulo strictness, efficiency
> etc) as the default one?
> 
> I don't know the answer to that.
> 
>> Agreed. I was about to answer that the situation is the same with the
>> monad laws not being valid for some monad we all love, and still we do
>> not consider the resulting programs illegal.
> 
> I do!  The H98 report says that all Monad instances must obey the monad
> laws.  If they don't, they're illegal.
> 
> (As an aside: The H98 report still list the right-zero law as being
> a law for MonadPlus, even though most MonadPlus instances don't obey
> it.  That's actually a defect in the report.)
> 
>> But your point about the
>> associativity law for Monoid is correct: these laws do not turn up as
>> preconditions for a free theorem.
> 
> Right.  And in that case, there's a clear reason why.
> 
> The precondition for (Alg a) essentially says that the mapping
> function g :: C1 -> C2 must be a Alg-homomorphism.  That implicitly
> assumes that C1 and C2 are both valid Alg-es, so if there are any
> "laws" of Alg, C1 and C2 both obey them by fiat.
> 
>> So we are back to those invariants that are expressed as default
>> instances. For Eq the invariant is quite obvious. But what about Ord?
>> Certainly there is also an invariant that can be observed from its
>> default instances, but I don't see how it could be read off
>> mechanically.
> 
> You could, from a dependency analysis, automatically work out a
> minimal set of methods which are needed to satisfy the class.  In
> the case of Ord, for example, it doesn't seem too hard to deduce
> that you could either use (==) and (<=), or (==) and compare.
> 
> (You can't, unfortunately, mechanically deduce that (==) can be
> defined in terms of compare, despite what the last sentence of section
> 6.3.2 in the report says.)
> 
> Now that I look at it, the report notes that:
> 
>     -- Note that (min x y, max x y) = (x,y) or (y,x)
> 
> but never says that this requirement is mandatory.
> 
>> A more general solution here would really be welcome.
> 
> In general, it'd be nice to be able to get the compiler to check that
> you've implemented at least a minimal set of operations in your class
> instance.
> 
> Cheers,
> Andrew Bromage
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
>