On 12/14/07, David Menendez <[EMAIL PROTECTED]> 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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
