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

[Kim-Ee Yeoh]

On Sun, Jan 17, 2016 at 10:17 AM, 鲍凯文 <traqueofziche at gmail.com> wrote:

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.
>

You've got the right idea. The general outline of a simple inductive proof
is this:

1. Prove for the smallest case (in this case, a tree with just one Leaf)

2. While assuming that the hypothesis holds for a small case, prove
hypothesis for the next case one up in size

3. Put 1 and 2 together to claim hypothesis for all cases

You've done 1.

You're stuck at 2 because you haven't yet found some measure of a "size" of
a Tree.

What are some common Tree measures you've seen?

-- Kim-Ee
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20160117/776e85e0/attachment.html>