[Haskell-beginners] proving fmap law for recursive data types

[鲍凯文]

Hi,

Suppose you have something like:

data Tree a = Leaf a | Branch (Tree a) (Tree a)

instance Functor Tree where
  fmap f (Leaf a) = Leaf $ f a
  fmap f (Branch l r) = Branch (fmap f l) (fmap f r)

To check that fmap id = id, I can see that the case for Leaf is ok:
  fmap id (Leaf a) = Leaf $ id a = Leaf a

How would you prove it for the second case? Is some sort of inductive proof
necessary? I found this:
http://ssomayyajula.github.io/posts/2015-11-07-proofs-of-functor-laws-with-Haskell.html,
which goes over an inductive (on the length of the list) proof for the list
type, but I'm not sure how to do it for a Tree.

Thanks,

toz
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20160116/5310632a/attachment.html>