
On 12/14/07, David Menendez
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