[Haskell-cafe] Re: lawless instances of Functor

[Luke Palmer]

On Mon, Jan 4, 2010 at 7:25 PM, Maciej Piechotka <uzytkownik2 at gmail.com> wrote:
> 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