Re: [Haskell-cafe] Class invariants/laws
Ryan Ingram wrote: On 10/18/07, Janis Voigtlaender <[EMAIL PROTECTED]> 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:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Class invariants/laws
Ha, well spotted! GHC's "RULE" mechanism is specifically designed to allow
library authors to add domain specific optimisations. Just as a library author
can write a buggy implementation of 'reverse', so s/he can write a buggy
optimisation rule.
So I guess it's up to the authors and maintainers of Control.Arrow to decide
whether they want to remove the rule, or simply advertise that instances of
Arrow had better obey it! In which case the libraries list is the place to
discuss.
Simon
| -Original Message-
| From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of Ryan
| Ingram
| Sent: 19 October 2007 07:01
| To: Simon Peyton-Jones
| Cc: haskell-cafe@haskell.org
| Subject: Re: [Haskell-cafe] Class invariants/laws
|
| 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.
|
| -- ryan
|
|
| On 10/18/07, Simon Peyton-Jones <[EMAIL PROTECTED]> 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?
| >
| > I don't believe GHC relies on any class laws. It'd be pretty dangerous to
do so, I think.
| >
| > Simon
| >
| ___
| 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] Class invariants/laws
On 10/18/07, Janis Voigtlaender <[EMAIL PROTECTED]> 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). The papers describing arrows clearly
state a set of laws which arrows are expected to follow, and the RULES
specify those laws clearly to anyone looking at the definition of
Arrow.
Also, for arrows in particular, which have hardwired compiler support,
it's more difficult for a user to separate "the library" from "the
compiler"; they go hand in hand.
> So I can, for example, write a rule that "sum xs" is zero for any list xs.
Sure, but you're not stating a valid law for lists. Now, if on the
other hand, you had:
-- Invariant: the elements of a ListZero to always sum to 0
newtype Num a => ListZero a = ListZero { unListZero :: [a] }
-- code to implement some useful operations on this type
{-# RULES "sum/unListZero" forall as. sum (unListZero as) = fromInteger 0 #-}
This rule would be valid according to the documentation specified.
It's not a big step from here to specifying the laws that instances of
a particular class must specify. That's what they're for, after all;
a typeclass is more than just overloading.
> 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. Having to restate the arrow laws as optimization rules for
each instance of Arrow would waste a lot of code, as well as requiring
people who implement an Arrow to know not just the Arrow laws but the
internals of GHC's optimization RULES system in order to get the
(often very significant) benefits of the compiler being able to
optimize based on those laws.
-- ryan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Class invariants/laws
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:[EMAIL PROTECTED]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Class invariants/laws
[EMAIL PROTECTED] wrote: 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. Yes, that's the standard motivation for allowing to implement more of the class methods than would actually be needed. But the "(or more lazy, or whatever)"-part bodes ill. If I understand correctly what you mean by "more lazy", it implies that you are willing to accept variations of complementary methods like (==) and (/=) that do satisfy the expected invariant, except for their behaviour with respect to partially defined inputs. But exactly this "up to bottom"-reasoning is what gets us into trouble with free theorems in Haskell. If you look at the class-respectance conditions generated for the language subset including selective strictness, you will find preconditions related to _|_. So it is dangerous to do both: 1. record only a subset of those restrictions based on the argument that the methods are anyway tied together via invariants 2. require those same invariants to hold "up to _|_" only The result would be free theorems that might be wrong for class instances that satisy the invariants suggested by default method implementations only in this lax way. Better, then, to go the full way and record the restrictions for all class methods, thus being prepared for *any* instance definition, be it fully compliant with the default method implementation, only laxly compliant, or not at all. 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] Class invariants/laws
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.
-- ryan
On 10/18/07, Simon Peyton-Jones <[EMAIL PROTECTED]> 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?
>
> I don't believe GHC relies on any class laws. It'd be pretty dangerous to do
> so, I think.
>
> Simon
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Class invariants/laws
G'day all. Quoting Janis Voigtlaender <[EMAIL PROTECTED]>: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Class invariants/laws
On 10/18/07, Simon Peyton-Jones <[EMAIL PROTECTED]> 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Class invariants/laws
| > 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? I don't believe GHC relies on any class laws. It'd be pretty dangerous to do so, I think. Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Class invariants/laws
[EMAIL PROTECTED] wrote: 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. Okay. I wasn't aware that the report makes this mandatory. 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. 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. 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
[Haskell-cafe] Class invariants/laws
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:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
