
16 Jan
2016
16 Jan
'16
10:17 p.m.
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-H..., 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