Re: [Haskell-cafe] Re: [Haskell] Announce: generating free theorems, online and offline
G'day. Quoting Janis Voigtlaender [EMAIL PROTECTED]: 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.) Unfortunately, the H98 report doesn't say this explicitly, so you're technically correct that such a misbehaving program is legal. Many invariants of this form are expressed as default instances, and if not, they should be. Obviously that's impossible in the case of, say, the associative law of Monoid. However, that isn't a precondition for a free theorem. Of course, it does not affect the correctness of the generated theorem, just its legibility. Of course. Consider this user feedback. :-) Cheers, Andrew Bromage ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] Announce: generating free theorems, online and offline
[EMAIL PROTECTED] wrote: G'day. Quoting Janis Voigtlaender [EMAIL PROTECTED]: 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:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] Announce: generating free theorems, online and offline
On 10/17/07, Janis Voigtlaender [EMAIL PROTECTED] wrote: 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? 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. 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. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] Announce: generating free theorems, online and offline
G'day all. Quoting Janis Voigtlaender [EMAIL PROTECTED]: 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
Re: [Haskell-cafe] Re: [Haskell] Announce: generating free theorems, online and offline
On Thu, Oct 18, 2007 at 03:36:01AM -0400, [EMAIL PROTECTED] 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 signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] Announce: generating free theorems, online and offline
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. [EMAIL PROTECTED] wrote: G'day all. Quoting Janis Voigtlaender [EMAIL PROTECTED]: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] Announce: generating free theorems, online and offline
On Thu, Oct 18, 2007 at 08:39:04PM -0400, David Menendez wrote: On 10/18/07, Stefan O'Rear [EMAIL PROTECTED] wrote: On Thu, Oct 18, 2007 at 03:36:01AM -0400, [EMAIL PROTECTED] 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 signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] Announce: generating free theorems, online and offline
On 10/18/07, Stefan O'Rear [EMAIL PROTECTED] wrote: On Thu, Oct 18, 2007 at 03:36:01AM -0400, [EMAIL PROTECTED] 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. -- Dave Menendez [EMAIL PROTECTED] http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] Announce: generating free theorems, online and offline
[EMAIL PROTECTED] wrote:
Some of these respects-restrictions arent as useful as they might be,
because they don't take into account easily-predictable invariants.
For example, the type:
(Eq a) = [a] - [a]
generates the following restriction:
g respects Eq if
forall x :: t1. forall y :: t1. (==) x y = (==) (g x) (g y)
forall x :: t1. forall y :: t1. (/=) x y = (/=) (g x) (g y)
Thats correct, but redundant, because (x == y) = (g x == g y) if and only
if (x /= y) = (g x /= g y). Crucially, you can work this out from the
definition of Eq, because (/=) has a default implementation defined in
terms of (==) alone.
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. If just requiring one of the two conditions
above, it is possible to write a function and instances of Eq so that
the theorem supposedly guaranteed by the function's type gets wrong.
The same applies to the Monoid example.
Also, the implementation is made for arbitrary user-declared type
classes, not just the ones from the standard libraries. It is easy to
parse the type signatures in a type class declaration. But to take
default method definitions into account as well, and automatically
working out the kind of redundancies that would allow to simplify
necessary restrictions, is next to impossible, I think.
Even more curiously, though, map
appears in the theorem, but lift{[]} appears in the class restriction.
Well-spotted. This was one of the small deficiencies that Sascha did not
come around to fix when time was running out towards the end of his MSc
thesis work on this project ;-)
Of course, it does not affect the correctness of the generated theorem,
just its legibility. In general, there are some other corners where one
could beneficially improve the amount of simplifications done. But my
most important point was to get *correct* statements out of the tool.
Overzealous simplification can easily compromise this aim (see above).
Ciao, Janis.
--
Dr. Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:[EMAIL PROTECTED]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
