Re: [Haskell-cafe] Questions about the Functor class and it's use in "Data types à la carte"
ryani.spam at gmail.com
Fri Dec 14 21:15:52 EST 2007
On 12/14/07, David Menendez <dave at zednenem.com> wrote:
> And yes, I'm pretty sure that's the only possible implementation for that
> type which satisfies the functor laws.
Lets just prove it, then; I'm pretty sure it comes pretty easily from the
free theorem for the type of fmap.
> data Val a = Val Int
> fmap :: (a -> b) -> (Val a -> Val b)
which must satisfy the law
fmap id1 = id2
id1 :: forall a. a -> a
id2 :: forall a. Val a -> Val a
Now, first note that since we cannot make any choices based on the type of
f, there's no way for f to be relevant to the result of fmap; we have no way
to get something of type "a" besides _|_ to pass to f, and no use for things
of type "b".
Therefore, since the choice of f can't affect the implementation of fmap, we
are given the only possible implementation directly from the Functor law:
fmap _ ~= id
or, to avoid the type error mentioned previously,
> fmap _ (Val x) = (Val x)
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe