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