[Haskell-cafe] Class invariants/laws

[Ryan Ingram]

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
>