Functions
Posted on 2018-01-30 by nbloomf
\(\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}\)
\(\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}\)
\(\newcommand{\a}{a}\)
\(\newcommand{\b}{b}\)
\(\newcommand{\c}{c}\)
\(\newcommand{\p}{p}\)
\(\newcommand{\q}{q}\)
\(\newcommand{\r}{r}\)
\(\newcommand{\s}{s}\)
\(\newcommand{\x}{x}\)
\(\newcommand{\y}{y}\)
\(\newcommand{\z}{z}\)
\(\newcommand{\bool}{\mathbb{B}}\)
\(\newcommand{\btrue}{\mathsf{true}}\)
\(\newcommand{\bfalse}{\mathsf{false}}\)
\(\newcommand{\bnot}{\mathsf{not}}\)
\(\newcommand{\band}{\mathbin{\mathsf{and}}}\)
\(\newcommand{\bor}{\mathbin{\mathsf{or}}}\)
\(\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}\)
\(\newcommand{\beq}{\mathsf{eq}}\)
\(\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}\)
\(\newcommand{\id}{\mathsf{id}}\)
\(\newcommand{\compose}{\mathsf{compose}}\)
\(\newcommand{\const}{\mathsf{const}}\)
\(\newcommand{\apply}{\mathsf{apply}}\)
\(\newcommand{\flip}{\mathsf{flip}}\)
\(\newcommand{\flipB}{\mathsf{flip2}}\)
\(\newcommand{\flipC}{\mathsf{flip3}}\)
\(\newcommand{\flipD}{\mathsf{flip4}}\)
\(\newcommand{\flipE}{\mathsf{flip5}}\)
\(\newcommand{\clone}{\mathsf{clone}}\)
\(\newcommand{\cloneC}{\mathsf{clone3}}\)
\(\newcommand{\composeAonB}{\mathsf{compose1on2}}\)
\(\newcommand{\composeAonC}{\mathsf{compose1on3}}\)
\(\newcommand{\composeAonD}{\mathsf{compose1on4}}\)
\(\newcommand{\composeBonA}{\mathsf{compose2on1}}\)
\(\newcommand{\composeBonB}{\mathsf{compose2on2}}\)
\(\newcommand{\composeConA}{\mathsf{compose3on1}}\)
\(\newcommand{\ptrue}{\mathsf{ptrue}}\)
\(\newcommand{\pfalse}{\mathsf{pfalse}}\)
\(\newcommand{\pnot}{\mathsf{pnot}}\)
\(\newcommand{\pand}{\mathbin{\mathsf{pand}}}\)
\(\newcommand{\por}{\mathbin{\mathsf{por}}}\)
\(\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}\)
\(\newcommand{\fst}{\mathsf{first}}\)
\(\newcommand{\snd}{\mathsf{second}}\)
\(\newcommand{\dup}{\mathsf{dup}}\)
\(\newcommand{\tup}{\mathsf{tup}}\)
\(\newcommand{\tSwap}{\mathsf{swap}_{\times}}\)
\(\newcommand{\tPair}{\mathsf{pair}_{\times}}\)
\(\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}\)
\(\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}\)
\(\newcommand{\tupL}{\mathsf{tupL}}\)
\(\newcommand{\tupR}{\mathsf{tupR}}\)
\(\newcommand{\uncurry}{\mathsf{uncurry}}\)
\(\newcommand{\curry}{\mathsf{curry}}\)
\(\newcommand{\lft}{\mathsf{left}}\)
\(\newcommand{\rgt}{\mathsf{right}}\)
\(\newcommand{\either}{\mathsf{either}}\)
\(\newcommand{\uSwap}{\mathsf{swap}_{+}}\)
\(\newcommand{\uPair}{\mathsf{pair}_{+}}\)
\(\newcommand{\uAssocL}{\mathsf{assocL}_{+}}\)
\(\newcommand{\uAssocR}{\mathsf{assocR}_{+}}\)
\(\newcommand{\isLft}{\mathsf{isLeft}}\)
\(\newcommand{\isRgt}{\mathsf{isRight}}\)
\(\newcommand{\nats}{\mathbb{N}}\)
\(\newcommand{\zero}{\mathsf{0}}\)
\(\newcommand{\next}{\mathsf{next}}\)
\(\newcommand{\unnext}{\mathsf{unnext}}\)
\(\newcommand{\iszero}{\mathsf{isZero}}\)
\(\newcommand{\prev}{\mathsf{prev}}\)
\(\newcommand{\natrec}{\mathsf{natrec}}\)
\(\newcommand{\simprec}{\mathsf{simprec}}\)
\(\newcommand{\bailrec}{\mathsf{bailrec}}\)
\(\newcommand{\mutrec}{\mathsf{mutrec}}\)
\(\newcommand{\dnatrec}{\mathsf{dnatrec}}\)
\(\newcommand{\normrec}{\mathsf{normrec}}\)
\(\newcommand{\findsmallest}{\mathsf{findsmallest}}\)
\(\newcommand{\mnormrec}{\mathsf{mnormrec}}\)
\(\newcommand{\nequal}{\mathsf{eq}}\)
\(\newcommand{\nplus}{\mathsf{plus}}\)
\(\newcommand{\ntimes}{\mathsf{times}}\)
\(\newcommand{\nleq}{\mathsf{leq}}\)
\(\newcommand{\ngeq}{\mathsf{geq}}\)
\(\newcommand{\nminus}{\mathsf{minus}}\)
\(\newcommand{\nmax}{\mathsf{max}}\)
\(\newcommand{\nmin}{\mathsf{min}}\)
\(\newcommand{\ndivalg}{\mathsf{divalg}}\)
\(\newcommand{\nquo}{\mathsf{quo}}\)
\(\newcommand{\nrem}{\mathsf{rem}}\)
\(\newcommand{\ndiv}{\mathsf{div}}\)
\(\newcommand{\ngcd}{\mathsf{gcd}}\)
\(\newcommand{\ncoprime}{\mathsf{coprime}}\)
\(\newcommand{\nlcm}{\mathsf{lcm}}\)
\(\newcommand{\nmindiv}{\mathsf{mindiv}}\)
\(\newcommand{\nisprime}{\mathsf{isPrime}}\)
\(\newcommand{\npower}{\mathsf{power}}\)
\(\newcommand{\nchoose}{\mathsf{choose}}\)
\(\newcommand{\dom}{\mathsf{dom}}\)
\(\newcommand{\cod}{\mathsf{cod}}\)
\(\newcommand{\lists}[1]{\mathsf{List}(#1)}\)
\(\newcommand{\nil}{\mathsf{nil}}\)
\(\newcommand{\cons}{\mathsf{cons}}\)
\(\newcommand{\uncons}{\mathsf{uncons}}\)
\(\newcommand{\isnil}{\mathsf{isNil}}\)
\(\newcommand{\tail}{\mathsf{tail}}\)
\(\newcommand{\head}{\mathsf{head}}\)
\(\newcommand{\foldr}{\mathsf{foldr}}\)
\(\newcommand{\foldl}{\mathsf{foldl}}\)
\(\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}\)
\(\newcommand{\unfoldN}{\mathsf{unfoldN}}\)
\(\newcommand{\dfoldr}{\mathsf{dfoldr}}\)
\(\newcommand{\cfoldr}{\mathsf{cfoldr}}\)
\(\newcommand{\bfoldr}{\mathsf{bfoldr}}\)
\(\newcommand{\dbfoldr}{\mathsf{dbfoldr}}\)
\(\newcommand{\lfoldr}{\mathsf{lfoldr}}\)
\(\newcommand{\snoc}{\mathsf{snoc}}\)
\(\newcommand{\revcat}{\mathsf{revcat}}\)
\(\newcommand{\rev}{\mathsf{rev}}\)
\(\newcommand{\last}{\mathsf{last}}\)
\(\newcommand{\cat}{\mathsf{cat}}\)
\(\newcommand{\addlength}{\mathsf{addlength}}\)
\(\newcommand{\length}{\mathsf{length}}\)
\(\newcommand{\head}{\mathsf{head}}\)
\(\newcommand{\at}{\mathsf{at}}\)
\(\newcommand{\map}{\mathsf{map}}\)
\(\newcommand{\range}{\mathsf{range}}\)
\(\newcommand{\zip}{\mathsf{zip}}\)
\(\newcommand{\zipPad}{\mathsf{zipPad}}\)
\(\newcommand{\unzip}{\mathsf{unzip}}\)
\(\newcommand{\prefix}{\mathsf{prefix}}\)
\(\newcommand{\suffix}{\mathsf{suffix}}\)
\(\newcommand{\lcp}{\mathsf{lcp}}\)
\(\newcommand{\lcs}{\mathsf{lcs}}\)
\(\newcommand{\all}{\mathsf{all}}\)
\(\newcommand{\any}{\mathsf{any}}\)
\(\newcommand{\tails}{\mathsf{tails}}\)
\(\newcommand{\inits}{\mathsf{inits}}\)
\(\newcommand{\filter}{\mathsf{filter}}\)
\(\newcommand{\elt}{\mathsf{elt}}\)
\(\newcommand{\addcount}{\mathsf{addcount}}\)
\(\newcommand{\count}{\mathsf{count}}\)
\(\newcommand{\repeat}{\mathsf{repeat}}\)
\(\newcommand{\sublist}{\mathsf{sublist}}\)
\(\newcommand{\infix}{\mathsf{infix}}\)
\(\newcommand{\select}{\mathsf{select}}\)
\(\newcommand{\unique}{\mathsf{unique}}\)
\(\newcommand{\delete}{\mathsf{delete}}\)
\(\newcommand{\dedupeL}{\mathsf{dedupeL}}\)
\(\newcommand{\dedupeR}{\mathsf{dedupeR}}\)
\(\newcommand{\common}{\mathsf{common}}\)
\(\newcommand{\disjoint}{\mathsf{disjoint}}\)
\(\newcommand{\sublists}{\mathsf{sublists}}\)
\(\newcommand{\take}{\mathsf{take}}\)
\(\newcommand{\drop}{\mathsf{drop}}\)
\(\newcommand{\takeBut}{\mathsf{takeBut}}\)
\(\newcommand{\dropBut}{\mathsf{dropBut}}\)
\(\newcommand{\takeWhile}{\mathsf{takeWhile}}\)
\(\newcommand{\dropWhile}{\mathsf{dropWhile}}\)
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.
Today we’ll nail down some generic functions.
Every set has an associated identity function.
Let \(A\) be a set. We define \(\id : A \rightarrow A\) by \(\id(x) = x\).
In Haskell:
Given two functions, one with domain \(B\) and the other with codomain \(B\), we can construct their composite.
Let \(A\), \(B\), and \(C\) be sets. Given \(f : A \rightarrow B\) and \(B : B \rightarrow C\), we define \(\compose(g)(f) : A \rightarrow C\) by \[\compose(g)(f)(x) = g(f(x)).\]
In Haskell:
\(\id\) is neutral under \(\compose(\ast)(\ast)\).
Let \(A\) and \(B\) be sets, with \(f : A \rightarrow B\). Then we have the following.
- \(\compose(\id)(f) = f\).
- \(\compose(f)(\id) = f\).
- Let \(a \in A\). Then we have \[\begin{eqnarray*}
& & \compose(\id)(f)(a) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-compose}
= & \id(f(a)) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-id}
= & f(a)
\end{eqnarray*}\] as needed.
- Let \(a \in A\). Then we have \[\begin{eqnarray*}
& & \compose(f)(\id)(a) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-compose}
= & f(\id(a)) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-id}
= & f(a)
\end{eqnarray*}\] as needed.
\(\compose(\ast)(\ast)\) is associative.
Let \(A\), \(B\), \(C\), and \(D\) be sets. For all \(f : A \rightarrow B\), \(g : B \rightarrow C\), and \(h : C \rightarrow D\), we have \[\compose(h)(\compose(g)(f)) = \compose(\compose(h)(g))(f).\]
Let \(a \in A\). Then we have \[\begin{eqnarray*}
& & \compose(h)(\compose(g)(f))(a) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-compose}
= & h(\compose(g)(f)(a)) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-compose}
= & h(g(f(a))) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-compose}
= & \compose(h)(g)(f(a)) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-compose}
= & \compose(\compose(h)(g))(f)(a)
\end{eqnarray*}\] as needed.
The \(\const\) function throws away its second argument.
Let \(A\) and \(B\) be sets. We define \(\const : B \rightarrow B^A\) by \[\const(b)(a) = b.\]
In Haskell:
\(\const(b)\) absorbs under \(\compose(\ast)(\ast)\) from the left.
Let \(A\), \(B\), and \(C\) be sets. For all \(f : A \rightarrow B\) and \(c \in C\) we have \[\compose(\const(c))(f) = \const(c).\]
Let \(a \in A\). Note that \[\begin{eqnarray*}
& & \compose(\const(c))(f)(a) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-compose}
= & \const(c)(f(a)) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-const}
= & c \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-const}
= & \const(c)(a)
\end{eqnarray*}\] as needed.
\(\apply\) is operatorized function application.
Given \(f : A \rightarrow B\) and \(x \in A\), we define \[\apply(f)(x) = f(x).\]
In Haskell:
\(\apply\) distributes over compose.
If \(f : A \rightarrow B\) and \(g : B \rightarrow C\) we have \[\apply(\compose(g)(f)) = \compose(\apply(g))(\apply(f)).\]
Let \(x \in A\). Now we have \[\begin{eqnarray*}
& & \apply(\compose(g)(f))(x) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-apply}
= & \compose(g)(f)(x) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-compose}
= & g(f(x)) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-apply}
= & \apply(g)(f(x)) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-apply}
= & \apply(g)(\apply(f)(x)) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-compose}
= & \compose(\apply(g))(\apply(f))(x)
\end{eqnarray*}\] as needed.
Testing
Suite:
_test_functions ::
( Equal a, Show a, Arbitrary a, CoArbitrary a, TypeName a
, Equal b, Show b, Arbitrary b, CoArbitrary b, TypeName b
, Equal c, Show c, Arbitrary c, CoArbitrary c, TypeName c
, Equal d, Show d, Arbitrary d, CoArbitrary d, TypeName d
) => Int -> Int -> a -> b -> c -> d -> IO ()
_test_functions size cases a b c d = do
testLabel0 "Functions"
let args = testArgs size cases
runTest args (_test_compose_id_left a b)
runTest args (_test_compose_id_right a b)
runTest args (_test_compose_associative a b c d)
runTest args (_test_compose_const_left a b c)
runTest args (_test_apply_compose_distribute a b c)
Main: