Law for type [[a]] -> ([a], [a])

Question

I am trying to do this question from my homework:

Given arbitrary foo :: [[a]] -> ([a], [a]), write down one law that the function foo satisfies, involving map on lists and pairs.

Some context: I am a first year undergrad taking a course of functional programming. Whilst the course is rather introductory, the lecturer has mentioned many things out of syllabus, amongst which are the free theorems. So after attempting to read Wadler's paper, I reckoned that concat :: [[a]] -> [a] with the law map f . concat = concat . map (map f) looks relevant to my problem, since we must have foo xss = (concat xss, concat' xss) where concat and concat' are any functions of type [[a]] -> [a]. Then foo satisfies bimap (map f, map g) . foo = \xss -> ((fst . foo . map (map f)) xss, (snd . foo . map (map g)) xss).

Already this 'law' seems too long to be correct, and I am unsure of my logic as well. So I thought of using an online free theorems generator, but I don't get what lift{(,)} means:

forall t1,t2 in TYPES, g :: t1 -> t2.
 forall x :: [[t1]].
  (f x, f (map (map g) x)) in lift{(,)}(map g,map g)

lift{(,)}(map g,map g)
  = {((x1, x2), (y1, y2)) | (map g x1 = y1) && (map g x2 = y2)}

How should I understand this output? And how should I derive the law for the function foo properly?

Answer 1

If R1 and R2 are relations (say, R_i between A_i and B_i, with i in {1,2}), then lift{(,)}(R1,R2) is the "lifted" relations pairs, between A1 * A2 and B1 * B2, with * denoting the product (written (,) in Haskell).

In the lifed relation, two pairs (x1,x2) :: A1*A2 and (y1,y2) :: B1*B2 are related if and only if x1 R1 y1 and x2 R2 y2. In your case, R1 and R2 are functions map g, map g, so the lifting becomes a function as well: y1 = map g x1 && y2 = map g x2.

Hence, the generated

(f x, f (map (map g) x)) in lift{(,)}(map g,map g)

means:

fst (f (map (map g) x)) = map g (fst (f x))
AND
snd (f (map (map g) x)) = map g (snd (f x))

or, in other words:

f (map (map g) x) = (map g (fst (f x)), map g (snd (f x)))

which I wold write as, using Control.Arrow:

f (map (map g) x) = (map g *** map g) (f x)

or even, in pointfree style:

f . map (map g) = (map g *** map g) . f

This is no surprise, since your f can be written as

f :: F a -> G a
where F a = [[a]]
      G a = ([a], [a])

and F,G are functors (in Haskell we would need to use a newtype to define a functor instance, but I will omit that, since it's irrelevant). In such common case, the free theorem has a very nice form: for every g,

f . fmap_of_F g = fmap_of_G g . f

This is a very nice form, called naturality (f can be interpreted as a natural transformation in a suitable category). Note that the two fs above are actually instantiated on separate types, so to make types agree with the rest.

In your specific case, since F a = [[a]], it is the composition of the [] functor with itself, hence we (unsurprisingly) get fmap_of_F g = fmap_of_[] (fmap_of_[] g) = map (map g).

Instead, G a = ([a],[a]) is the composition of functors [] and H a = (a,a) (technically, diagonal functor composed with the product functor). We have fmap_of_H h = (h *** h) = (\x -> (h x, h x)), from which fmap_of_G g = fmap_of_H (fmap_of_[] g) = (map g *** map g).

Answer 2

Same thing as @chi's answer with less ceremony:

It doesn't matter if you change the as to bs before or after the function, you get the same thing (as long as you use an fmap-like-thing to do it).

For any f : a -> b,

    [[a]] ------------->   [[b]]
      |    (map.map) f       |
      |                      |
     foo                    foo
      |                      |
      v                      v
    ([a],[a]) ---------> ([b],[b])
              bimap f f

commutes.