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

[ajb at spamcop.net]

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