proving fmap law for recursive data types

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

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


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: proving fmap law for recursive data types

Kim-Ee Yeoh
Administrator

On Sun, Jan 17, 2016 at 10:17 AM, 鲍凯文 <[hidden email]> 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

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners