Re: [Haskell-cafe] Questions about the Functor class and it's use in "Data types à la carte"

[Ryan Ingram]

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

with
  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)

  -- ryan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20071214/5ecb0e64/attachment.htm