# Map

Posted on 2017-04-29 by nbloomf

This post is literate Haskell; you can load the source into GHCi and play along.

{-# LANGUAGE NoImplicitPrelude #-}
module Map
( map, _test_map, main_map
) where

import Testing
import Functions
import DisjointUnions
import NaturalNumbers
import Lists
import Snoc
import Reverse
import Cat
import Length
import At

Today we’ll explore one of the most useful functions on $$\lists{A}$$: $$\map$$. What $$\map$$ does is take a function $$A \rightarrow B$$ and a $$\lists{A}$$, and apply the function “itemwise” to get a $$\lists{B}$$.

Let $$A$$ and $$B$$ be sets. We then define $$\map : B^A \rightarrow \lists{A} \rightarrow \lists{B}$$ by $\map(f) = \foldr(\nil)(\compose(\cons)(f)).$

map :: (List t) => (a -> b) -> t a -> t b
map f = foldr nil (compose cons f)

Since $$\map$$ is defined as a $$\foldr(\ast)(\ast)$$, it is the unique solution to a system of functional equations.

$$\map(\alpha)$$ is the unique solution $$f : \lists{A} \rightarrow \lists{B}$$ of the following equations for all $$a \in A$$ and $$x \in \lists{A}$$: $\left\{\begin{array}{l} f(\nil) = \nil \\ f(\cons(a,x)) = \cons(\alpha(a),f(x)) \end{array}\right.$

_test_map_nil :: (List t, Equal (t a))
=> t a -> Test ((a -> a) -> Bool)
_test_map_nil t =
testName "map(f)(nil) == nil" $\f -> eq (map f (nil withTypeOf t)) nil _test_map_cons :: (List t, Equal (t a)) => t a -> Test ((a -> a) -> a -> t a -> Bool) _test_map_cons _ = testName "map(f)(cons(a,x)) == cons(f(a),map(f)(x))"$
\f a x -> eq (map f (cons a x)) (cons (f a) (map f x))

One way to think about $$\map$$ is that it fills in the following diagram. $\require{AMScd} \begin{CD} A @>{f}>> B\\ @V{\lists{\ast}}VV @VV{\lists{\ast}}V \\ \lists{A} @>>{\map(f)}> \lists{B} \end{CD}$ This looks an awful lot like a functor diagram. Recall that given two categories, a functor associates objects to objects and morphisms to morphisms, preserving $$\id$$ and composition. And indeed, $$\map$$ is the morphism part of the $$\lists{\ast}$$ functor.

$$\map$$ takes $$\id_A$$ to $$\id_{\lists{A}}$$.

Let $$A$$ be a set. Then we have $\map(\id_A)(x) = x.$

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \map(\id)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \nil \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $$f$$ for some $$x$$ and let $$a \in A$$. Now $\begin{eqnarray*} & & \map(\id)(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \cons(\id(a),\map(\id)(x)) \\ & \hyp{\map(\id)(x) = x} = & \cons(\id(a),x) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-id} = & \cons(a,x) \end{eqnarray*}$ as needed.

_test_map_id :: (List t, Equal (t a))
=> t a -> Test (t a -> Bool)
_test_map_id _ =
testName "map(id)(x) == x" $\x -> eq (map id x) x $$\map$$ preserves composition. Let $$A$$, $$B$$, and $$C$$ be sets, with maps $$f : A \rightarrow B$$ and $$g : B \rightarrow C$$. For all $$x \in \lists{A}$$ we have $\map(\compose(g)(f))(x) = \compose(\map(g))(\map(f))(x).$ We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \compose(\map(g))(\map(f))(\nil) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \map(g)(\map(f)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \map(g)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \nil \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \map(\compose(g)(f))(\nil) \end{eqnarray*}$ as claimed. Suppose now that the equality holds for some $$x \in \lists{A}$$ and let $$a \in A$$. Then we have $\begin{eqnarray*} & & \compose(\map(g))(\map(f))(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \map(g)(\map(f)(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \map(g)(\cons(f(a),\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \cons(g(f(a)),\map(g)(\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \cons(\compose(g)(f)(a),\map(g)(\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \cons(\compose(g)(f)(a),\compose(\map(g))(\map(f))(x)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-map-compose} = & \cons(\compose(g)(f)(a),\map(\compose(g)(f))(x)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \map(\compose(g)(f))(\cons(a,x)) \end{eqnarray*}$ as needed. _test_map_compose :: (List t, Equal (t a)) => t a -> Test ((a -> a) -> (a -> a) -> t a -> Bool) _test_map_compose _ = testName "map(g . f)(x) == (map(g) . map(f))(x)"$
\g f x -> eq (map (g . f) x) (((map g) . (map f)) x)

$$\map(f)$$ respects $$\tail$$.

Let $$A$$ and $$B$$ be sets with a map $$f : A \rightarrow B$$. For all $$x \in \lists{A}$$, we have $\map(f)(\tail(x)) = \tail(\map(f)(x)).$

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \map(f)(\tail(\nil)) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-tail-nil} = & \map(f)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \nil \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-tail-nil} = & \tail(\nil) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \tail(\map(f)(\nil)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $$x$$ and let $$a \in A$$. Then $\begin{eqnarray*} & & \map(f)(\tail(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-tail-cons} = & \map(f)(x) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-tail-cons} = & \tail(\cons(f(a),\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \tail(\map(f)(\cons(a,x))) \end{eqnarray*}$ as needed.

_test_map_tail :: (List t, Equal (t a))
=> t a -> Test ((a -> a) -> t a -> Bool)
_test_map_tail _ =
testName "map(f)(tail(x)) == tail(map(f)(x))" $\f x -> eq (map f (tail x)) (tail (map f x)) $$\map(f)$$ respects $$\cat$$. Let $$A$$ and $$B$$ be sets with a map $$f : A \rightarrow B$$. For all $$x,y \in \lists{A}$$, we have $\map(f)(\cat(x,y)) = \cat(\map(f)(x),\map(f)(y)).$ We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \map(f)(\cat(\nil,y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \map(f)(y) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \cat(\nil,\map(f)(y)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \cat(\map(f)(\nil),\map(f)(y)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $$x \in \lists{A}$$ and let $$a \in A$$. Now $\begin{eqnarray*} & & \map(f)(\cat(\cons(a,x),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \map(f)(\cons(a,\cat(x,y))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \cons(f(a),\map(f)(\cat(x,y))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-map-cat} = & \cons(f(a),\cat(\map(f)(x),\map(f)(y))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \cat(\cons(f(a),\map(f)(x)),\map(f)(y)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \cat(\map(f)(\cons(a,x)),\map(f)(y)) \end{eqnarray*}$ as needed. _test_map_cat :: (List t, Equal (t a)) => t a -> Test ((a -> a) -> t a -> t a -> Bool) _test_map_cat _ = testName "map(f)(cat(x,y)) == cat(map(f)(x),map(f)(y))"$
\f x y -> eq (map f (cat x y)) (cat (map f x) (map f y))

$$\map(f)$$ respects $$\snoc$$.

Let $$A$$ and $$B$$ be sets with a map $$f : A \rightarrow B$$. For all $$a \in A$$ and $$x \in \lists{A}$$, we have $\map(f)(\snoc(a,x)) = \snoc(f(a),\map(f)(x)).$

We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \map(f)(\snoc(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \map(f)(\cons(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \cons(f(a),\map(f)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \cons(f(a),\nil) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \snoc(f(a),\nil) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \snoc(f(a),\map(f)(\nil)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $$f$$ and $$a$$ for some $$x$$, and let $$b \in A$$. Now $\begin{eqnarray*} & & \map(f)(\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \map(f)(\cons(b,\snoc(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \cons(f(b),\map(f)(\snoc(a,x))) \\ & \hyp{\map(f)(\snoc(a,x)) = \snoc(f(a),\map(f)(x))} = & \cons(f(b),\snoc(f(a),\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \snoc(f(a),\cons(f(b),\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \snoc(f(a),\map(f)(\cons(b,x))) \end{eqnarray*}$ as needed.

_test_map_snoc :: (List t, Equal (t a))
=> t a -> Test ((a -> a) -> a -> t a -> Bool)
_test_map_snoc _ =
testName "map(f)(snoc(a,x)) == snoc(f(a),map(f)(x))" $\f a x -> eq (map f (snoc a x)) (snoc (f a) (map f x)) $$\map(f)$$ respects $$\rev$$. Let $$A$$ and $$B$$ be sets with a map $$f : A \rightarrow B$$. For all $$x \in \lists{A}$$, we have $\map(f)(\rev(x)) = \rev(\map(f)(x)).$ We proceed by list induction on $$x$$. For the base case $$x = \nil$$, we have $\begin{eqnarray*} & & \map(f)(\rev(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \map(f)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \nil \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \rev(\nil) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \rev(\map(f)(\nil)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equation holds for some $$x \in \lists{A}$$ and let $$a \in A$$. Now $\begin{eqnarray*} & & \map(f)(\rev(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \map(f)(\snoc(a,\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#thm-map-snoc} = & \snoc(f(a),\map(f)(\rev(x))) \\ & \hyp{\map(f)(\rev(x)) = \rev(\map(f)(x))} = & \snoc(f(a),\rev(\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \rev(\cons(f(a),\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \rev(\map(f)(\cons(a,x))) \end{eqnarray*}$ as needed. _test_map_rev :: (List t, Equal (t a)) => t a -> Test ((a -> a) -> t a -> Bool) _test_map_rev _ = testName "map(f)(rev(x)) == rev(map(f)(x))"$
\f x -> eq (map f (rev x)) (rev (map f x))

$$\map(f)$$ interacts with $$\at$$:

Let $$A$$ and $$B$$ be sets with a map $$f : A \rightarrow B$$ and $$x \in \lists{A}$$. Then we have $\at(\map(f)(x),k) = \uPair(\id,f)(\at(x,k)).$

There are two possibilities for $$x$$. If $$x = \nil$$, we have $\begin{eqnarray*} & & \at(\map(f)(\nil),k) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \at(\nil,k) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-nil} = & \lft(\ast) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-id} = & \lft(\id(\ast)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uPair-lft} = & \uPair(\id,f)(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-nil} = & \uPair(\id,f)(\at(\nil,k)) \end{eqnarray*}$ as claimed. Suppose instead that $$x = \cons(a,y)$$. We now proceed by induction on $$k$$. For the base case $$k = \zero$$, we have $\begin{eqnarray*} & & \at(\map(f)(\cons(a,y)),\zero) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \at(\cons(f(a),\map(f)(y)),\zero) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-zero} = & \rgt(f(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uPair-rgt} = & \uPair(\id,f)(\rgt(a)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-zero} = & \uPair(\id,f)(\at(\cons(a,y),\zero)) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for all $$a$$ and $$y$$ for some $$k$$. Now $\begin{eqnarray*} & & \at(\map(f)(\cons(a,y)),\next(k)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \at(\cons(f(a),\map(f)(y)),\next(k)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-next} = & \at(\map(f)(y),k) \\ & \hyp{\at(\map(f)(x),k) = \uPair(\id,f)(\at(y,k))} = & \uPair(\id,f)(\at(y,k)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-next} = & \uPair(\id,f)(\at(\cons(a,y),\next(k))) \end{eqnarray*}$ as needed.

_test_map_at :: (List t, Equal (t a), Natural n, Equal n, Equal a)
=> t a -> n -> Test ((a -> a) -> t a -> n -> Bool)
_test_map_at _ _ =
testName "at(map(f)(x),k) == upair(id,f)(at(x,k))" $\f x k -> eq (at (map f x) k) (upair id f (at x k)) And $$\map$$ preserves $$\length$$. Let $$A$$ and $$B$$ be sets with a map $$f : A \rightarrow B$$. Then for all $$x \in \lists{A}$$ we have $\length(\map(f)(x)) = \length(x).$ We proceed by list induction on $$x$$. For the base case $$x = \nil$$ we have $\begin{eqnarray*} & & \length(\map(f)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \length(\nil) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $$x$$ and let $$a \in A$$. Now $\begin{eqnarray*} & & \length(\map(f)(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \length(\cons(f(a),\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \next(\length(\map(f)(x))) \\ & \hyp{\length(\map(f)(x)) = \length(x)} = & \next(\length(x)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \length(\cons(a,x)) \end{eqnarray*}$ as claimed. _test_map_length :: (List t, Equal (t a), Natural n, Equal n, Equal a) => t a -> n -> Test ((a -> a) -> t a -> Bool) _test_map_length _ k = testName "length(map(f)(x)) == length(x)"$
\f x -> eq (length (map f x)) ((length x) withTypeOf k)

$$\map$$ preserves $$\isnil$$.

Let $$A$$ and $$B$$ be sets with $$f : A \rightarrow B$$. For all $$x \in \lists{A}$$, we have $\isnil(\map(f)(x)) = \isnil(x).$

We have two possibilities for $$x$$. If $$x = \nil$$ we have $\begin{eqnarray*} & & \isnil(\map(f)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \isnil(\nil) \end{eqnarray*}$ and if $$x = \cons(a,u)$$ we have $\begin{eqnarray*} & & \isnil(\map(f)(\cons(a,u))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \isnil(\cons(f(a),\map(f)(u))) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-cons} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-cons} = & \isnil(\cons(a,u)) \end{eqnarray*}$ as needed.

_test_map_isnil :: (List t, Equal (t a))
=> t a -> Test ((a -> a) -> t a -> Bool)
_test_map_isnil _ =
testName "isnil(map(f)(x)) == isnil(x)" \$
\f x -> eq (isNil (map f x)) (isNil x)

## Testing

Suite:

_test_map ::
( TypeName a, Show a, Equal a, Arbitrary a, CoArbitrary a
, TypeName (t a), List t, Equal (t a), Arbitrary (t a), Show (t a)
, TypeName n, Show n, Equal n, Natural n, Arbitrary n
) => Int -> Int -> t a -> n -> IO ()
_test_map size cases t n = do
testLabel1 "map" t
let args = testArgs size cases

runTest args (_test_map_nil t)
runTest args (_test_map_cons t)
runTest args (_test_map_id t)
runTest args (_test_map_compose t)
runTest args (_test_map_tail t)
runTest args (_test_map_cat t)
runTest args (_test_map_snoc t)
runTest args (_test_map_rev t)
runTest args (_test_map_at t n)
runTest args (_test_map_length t n)
runTest args (_test_map_isnil t)

Main:

main_map :: IO ()
main_map = do
_test_map 20 100 (nil :: ConsList Bool)  (zero :: Unary)
_test_map 20 100 (nil :: ConsList Unary) (zero :: Unary)