[Haskell-cafe] Re: [Haskell] Announce: generating free
theorems, online and offline
ajb at spamcop.net
ajb at spamcop.net
Thu Oct 18 03:36:01 EDT 2007
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
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
More information about the Haskell-Cafe