On Mon, Jan 4, 2010 at 7:25 PM, Maciej Piechotka
On Tue, 2010-01-05 at 08:01 +0900, Derek Elkins wrote:
If h . p = q . g then fmap h . fmap p = fmap q . fmap g Setting p = id gives h . id = h = q . g && fmap h . fmap id = fmap q . fmap g Using fmap id = id and h = q . g we get, fmap h . fmap id = fmap h . id = fmap h = fmap (q . g) = fmap q . fmap g
Hmm. Not quite a proff as we want to use: For all f g fmap (f . g) = fmap f . fmap g. So we need to operate on arbitrary f and g. Also in first line conclusion is used - at this stage we don't know if h . p = p . q -> fmap h . fmap p = fmap q . fmap g.
No, the first line is the "free theorem" -- i.e. the parametericity theorem -- for the type. It holds for any Haskell value with this type, coming essentially from the fact that downcasts are not possible in Haskell. You can play with free theorems here: http://linux.tcs.inf.tu-dresden.de/~voigt/ft/. See Wadler's paper "Theorem's for free!" for more about them.
Especially that (A->B) functions is |A|^|B| (and in haskell |A| >= 1, | B| >= 1). Now imagine that (in pseudocode[1]): rho :: (A -> B) -> A -> B rho f | f is A -> A = id | f is Integral -> Integral = (+1) . fromIntegral | otherise = f
Haskell's inability to write this function is exactly where free theorems come from. Luke