[Haskell-cafe] Re: lawless instances of Functor
Luke Palmer
lrpalmer at gmail.com
Tue Jan 5 03:23:14 EST 2010
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
More information about the Haskell-Cafe
mailing list