Write proofs of the following facts in Haskell, along the lines of the Proofs lecture notes.

1. The type family + is commutative.
2. The type family + is associative.
3. The type family * (as defined in the VecList lecture notes) is commutative.

Write the following functions, also adapted from their list versions.

You will need VecList for most of these.

Also, for reasons we have not yet had the chance to discuss, type families do not participate in currying. You thus cannot cleverly write the Map type family and expect to say Map (+ 3) .... It won’t work. You can say Map Succ ... because Succ is not a type family. This might mean you have to write a few type families for the following problems that you would ordinarily get by using higher-order functions and currying.

Lastly, these are quite a big step harder than the problems you have already worked on. Other than intersperse (which is hard, but not like the others), view these as challenge problems. Enjoy the challenge. If you’re not enjoying it, stop. :)

1. intersperse
2. inits (You will need several new type families for this one. Write it on lists first as a warmup.)
3. tails (Ditto.)
4. intercalate (I found this to be pretty hard.)
5. subsequences (I have not tried this one myself. It looks hard, but doable.)
6. permutations (I have not tried this one myself. It looks hard, but doable.)
7. transpose (Thinking about this makes me want to cry. But maybe you will enjoy it as a challenge problem.)