G'day all. Quoting Derek Elkins <derek.a.elk...@gmail.com>:
Ignoring bottoms the free theorem for fmap can be written: 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
Dan Piponi points out:
When I play with http://haskell.as9x.info/ft.html I get examples that look more like: If fmap' has the same signature as the usual fmap for a type and h . p = q . g then fmap h . fmap' p = fmap' q . fmap g From which it follows that if fmap' id = id then fmap' is fmap.
The free theorem for: fmap' :: forall a b. (a -> b) -> F a -> F b assumes that F is already a Functor. That is, it shows that if there exists a valid fmap instance for F, then for any other function fmap' with the same signature as fmap, fmap' id = id implies fmap' = fmap. So if you want to invent a data type and fmap instance which satisfies law 1 but not law 2, then it needs to be a data type for which no valid fmap instance is possible *at all*. So it doesn't rule out the possibility completely, but it narrows down the search space considerably. Cheers, Andrew Bromage _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
