ajb@spamcop.net wrote:

G'day.

Quoting Janis Voigtlaender :

...

Hmm, but I can easily define an instance of Eq that does not satisfy this invariant. And I want the generated free theorem to be true for any legal Haskell program.

I would think that if x == y isn't the same as not (x /= y) for some type, then it isn't a legal Haskell program, because it breaks a fairly obvious invariant of Eq. (The consensus on #haskell is that this is even true for NaNs, but I'd like to get an official ruling on that.)

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?

Many invariants of this form are expressed as default instances, and if not, they should be.

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. But your point about the associativity law for Monoid is correct: these laws do not turn up as preconditions for a free theorem. 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. And that's really the point of free theorems: to get as far as possible with an automated process. Afterwards, one can always simplify by using knowledge not possibly available to the generation algorithm. So if for the Eq-instances we are actually interested in we really know that the invariant holds, we can of course do away with one of the two (==)-, (/=)-conditions. Alternatively, it would be possible to hard-code special treatment of Haskell's standard type classes into Sascha's tool, so that for Eq, Ord, and so on, a minimal set of conditions is imposed from the outset. But that would not help in general with type classes specified by the user. A more general solution here would really be welcome.

...

Of course, it does not affect the correctness of the generated theorem, just its legibility.

Of course. Consider this user feedback. :-)

Sure. More wanted :-) Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

Ryan Ingram wrote:

These invariants are basically impossible to enforce by the compiler, but nonetheless certain classes have laws which are expected to hold, and I would not be surprised if (for example) GHC optimization RULES depended on them.

I, in fact, would be surprised if there were such dependencies. (Not that there might not be good reasons to want to rely on such laws for some conceivable optimization, I just doubt that any implementation actually does.) Simon?

For example, there's no way to enforce that the implementation of >>= is associative, but it's nonetheless stated in the description of Monad and code assumes it to be true.

Do you have an example of such code? Anyway, how can code "assume" >>= to be associative? It would not make any difference for code whether or not >>= is associative. What is, of course, possible is that programmers assume >>= to be associative when doing refactorings of their code, such as juggling with do-notation. As far as implementations are concerned, I would conjecture that they all implement the single translation from do-notation to >>=-notation specified in the report. No need for any assumptions about associativity there. I might be wrong. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

On 10/18/07, Simon Peyton-Jones wrote:

I don't believe GHC relies on any class laws. It'd be pretty dangerous to do so, I think.

Incidentally, I consider it a slight infelicity that the H98 spec doesn't seem to mention the implied laws of classes like Eq and Ord, not even to disclaim responsibility for them. Even if the standard doesn't require that the laws hold, I suggest that it should at least state this explicitly, and perhaps recommend that they be obeyed. Is this something that might change in Haskell-Prime? Stuart

Ryan Ingram wrote:

Just today I was looking at the implementation of Arrows and noticed this:

{-# RULES "compose/arr" forall f g . arr f >>> arr g = arr (f >>> g) ... other rules ... #-}

But consider this "Arrow": newtype (a :>> b) = LA2 { runLA2 :: [a] -> [b] }

instance Arrow (:>>) where arr = LA2 . map LA2 ab >>> LA2 bc = LA2 $ \la -> let dupe [] = [] dupe (x:xs) = (x : x : dupe xs) lb = dupe (ab la) in bc lb first (LA2 f) = LA2 $ \l -> let (as,bs) = unzip l in zip (f as) bs

runLA2 (arr (+1) >>> arr (+1)) [1,2,3] => [3,3,4,4,5,5]

runLA2 (arr ((+1) >>> (+1))) [1,2,3] => [3,4,5]

Now, the RULE clearly states one of the arrow laws, so it's sound for any real Arrow, and :>> is clearly not a real Arrow. But, :>> satisfies the "compiles" restriction and breaks the validity of the RULE.

Yes, but that's a problem of the Arrow library writer, not of GHC. The compiler will never check a RULE. So I can, for example, write a rule that "sum xs" is zero for any list xs. I think what Simon was asserting is that none of the internal logic of GHC assumes any laws to hold for any type classes. If the programmer tricks the compiler by providing wrong RULES in source files, it's the programmers problem and fault. It's like using unsafePerformIO. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

Ryan Ingram wrote:

On 10/18/07, Janis Voigtlaender wrote:

...

Yes, but that's a problem of the Arrow library writer, not of GHC. The compiler will never check a RULE.

I'm going to disagree a bit here; it's not the problem of the Arrow library writer at all, it's the problem of the implementor of the faulty arrow (me, in this case).

Yes, it's an issue between you and the Arrow library writer, not between you and GHC.

...

I think what Simon was asserting is that none of the internal logic of GHC assumes any laws to hold for any type classes.

If that's the case, it doesn't address my original point at all, which was talking about the applicability of class laws to optimization RULES.

Your original point was that GHC optimization RULES might depend on class laws. That's obviously true, since anyone can write RULES in source code. What I find reasserting about Simon's statement is that no RULES (or other logic) that happen outside the control of the programmer will depend on class laws being true. Note that GHC internally generates RULES for some optimization tasks, without the compiler user having the least inkling. It could easily have been the case that so it also introduces an associativity law for >>= as given in the H98 report. Only then I would see how code depends on that law actually being true. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

G'day all. Quoting Janis Voigtlaender :

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

G'day all. Quoting Janis Voigtlaender :

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. Probably not true of (==) vs (/=), but it's often true of (<=) vs compare. Cheers, Andrew Bromage

On Thu, Oct 18, 2007 at 03:36:01AM -0400, ajb@spamcop.net wrote:

(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.)

All the MonadPlus I can think of (IO,Maybe,[]) satisfy it. Were you thinking of right distribution? Stefan

On Thu, Oct 18, 2007 at 08:39:04PM -0400, David Menendez wrote:

On 10/18/07, Stefan O'Rear wrote:

...

On Thu, Oct 18, 2007 at 03:36:01AM -0400, ajb@spamcop.net wrote:

...

(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.)

All the MonadPlus I can think of (IO,Maybe,[]) satisfy it. Were you thinking of right distribution?

"print 1 >> mzero" returns the same result as "mzero" (i.e., it throws an exception), but it has different effects.

Oh, hehe. I thought you meant print 1 `mappend` mzero being equal to print 1. Oops. Stefan

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@spamcop.net wrote:

G'day all.

Quoting Janis Voigtlaender :

...

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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe