[Haskell-cafe] Class invariants/laws

[Janis Voigtlaender]

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 at tcs.inf.tu-dresden.de