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