I am trying to do this question from my homework:
Given arbitrary
foo :: [[a]] -> ([a], [a])
, write down one law that the functionfoo
satisfies, involvingmap
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?
If
R1
andR2
are relations (say,R_i
betweenA_i
andB_i
, withi in {1,2}
), thenlift{(,)}(R1,R2)
is the "lifted" relations pairs, betweenA1 * A2
andB1 * 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 ifx1 R1 y1
andx2 R2 y2
. In your case,R1
andR2
are functionsmap g, map g
, so the lifting becomes a function as well:y1 = map g x1 && y2 = map g x2
.Hence, the generated
means:
or, in other words:
which I wold write as, using
Control.Arrow
:or even, in pointfree style:
This is no surprise, since your
f
can be written asand
F
,G
are functors (in Haskell we would need to use anewtype
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 everyg
,This is a very nice form, called naturality (
f
can be interpreted as a natural transformation in a suitable category). Note that the twof
s 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) getfmap_of_F g = fmap_of_[] (fmap_of_[] g) = map (map g)
.Instead,
G a = ([a],[a])
is the composition of functors[]
andH a = (a,a)
(technically, diagonal functor composed with the product functor). We havefmap_of_H h = (h *** h) = (\x -> (h x, h x))
, from whichfmap_of_G g = fmap_of_H (fmap_of_[] g) = (map g *** map g)
.