[Haskell-cafe] Class invariants/laws

[Simon Peyton-Jones]

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: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-bounces at haskell.org] On Behalf Of Ryan
| Ingram
| Sent: 19 October 2007 07:01
| To: Simon Peyton-Jones
| Cc: haskell-cafe at 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 <simonpj at microsoft.com> 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe