Map

Posted on 2017-04-29 by nbloomf
Tags: arithmetic-made-difficult, literate-haskell

This page is part of a series on Arithmetic Made Difficult.

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 HeadAndTail
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)).\]

In Haskell:

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.\]

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.

\(\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.

\(\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.

\(\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.

\(\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.

\(\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.

\(\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.

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.

\(\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.

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)