Tuples
Posted on 2014-04-02 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.
{-# LANGUAGE NoImplicitPrelude, FlexibleContexts #-}
module Tuples
( Pair(Pair,fst,snd), dup, tup, tswap, tpair, tassocL, tassocR
, uncurry, curry, _test_tuple, main_tuple
) where
import Testing
import Functions
import Flip
import Clone
import Composition
import Booleans
import AndToday we’ll establish a few basic utility functions on tuples. First, recall some definitions.
Let \(A\) and \(B\) be sets. There is a set \(A \times B\) together with two functions \(\fst : A \times B \rightarrow A\) and \(\snd : A \times B \rightarrow B\) having the property that if \(X\) is a set and \(\sigma : X \rightarrow A\) and \(\tau : X \rightarrow B\) functions then there is a unique map \(\Theta : X \rightarrow A \times B\) such that \(\fst \circ \Theta = \sigma\) and \(\snd \circ \Theta = \tau\). That is, there is a unique \(\Theta\) such that the following diagram commutes.
\[\require{AMScd} \begin{CD} X @= X @= X \\ @V{\sigma}VV @VV{\Theta}V @VV{\tau}V \\ A @<<{\fst}< A \times B @>>{\snd}> B \end{CD}\]
We will denote this unique \(\Theta : X \rightarrow A \times B\) by \(\dup(\sigma,\tau)\).
More concretely, if \(f : X \rightarrow A \times B\) such that \(\fst(f(x)) = \sigma(x)\) and \(\snd(f(x)) = \tau(x)\) for all \(x \in X\), then \(f = \dup(\sigma,\tau)\).
Now \(A \times B\) uniquely represents all possible pairs of elements of \(A\) and \(B\) in a precise sense.
Let \(A\) and \(B\) be sets. Given \(a \in A\) and \(b \in B\), we define \(\tup : A \rightarrow B \rightarrow A \times B\) by \[\tup(a)(b) = \dup(\const(a),\const(b))(\ast).\] Now we have the following.
- \(\fst(\tup(a)(b)) = a\) and \(\snd(\tup(a)(b)) = b\).
- If \(w \in A \times B\) such that \(\fst(w) = a\) and \(\snd(w) = b\), then \(w = \tup(a)(b)\).
- \(\beq(\tup(a)(b),\tup(c)(d)) = \band(\beq(a,c),\beq(b,d))\).
- We have \[\begin{eqnarray*} & & \fst(\tup(a)(b)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-tup} = & \fst(\dup(\const(a),\const(b))(\ast)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-fst-dup} = & \const(a)(\ast) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & a \end{eqnarray*}\] and \[\begin{eqnarray*} & & \snd(\tup(a)(b)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-tup} = & \snd(\dup(\const(a),\const(b))(\ast)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-snd-dup} = & \const(b)(\ast) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & b \end{eqnarray*}\] as claimed.
- Suppose \(\fst(w) = a\) and \(\snd(w) = b\), and consider \(\const(w)\) as a function \(\ast \rightarrow A \times B\). Note that \[\begin{eqnarray*} & & \fst(\const(w)(\ast)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \fst(w) \\ & \hyp{\fst(w) = a} = & a \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \const(a)(\ast) \end{eqnarray*}\] and \[\begin{eqnarray*} & & \snd(\const(w)(\ast)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \snd(w) \\ & \hyp{\snd(w) = b} = & b \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \const(b)(\ast) \end{eqnarray*}\] so by the universal property of \(A \times B\), \(w = \tup(a)(b)\).
- First suppose that \[\beq(\tup(a)(b),\tup(c)(d));\] then \[a = \fst(\tup(a)(b)) = \fst(\tup(c)(d)) = c\] and \[b = \snd(\tup(a)(b)) = \snd(\tup(c)(d)) = d\] so that \[\band(\beq(a,c),\beq(b,d)).\] Conversely, suppose \(\band(\beq(a,c),\beq(b,d))\). Then we have \[\fst(\tup(a)(b)) = a = c = \fst(\tup(c)(d))\] and \[\snd(\tup(a)(b)) = b = d = \snd(\tup(c)(d)).\] By (2), we have \(\tup(a)(b) = \tup(c)(d)\).
In Haskell we can model \(A \times B\), and the maps in the universal property, with the following type.
data Pair a b = Pair
{ fst :: a
, snd :: b
} deriving Show
dup :: (x -> a) -> (x -> b) -> x -> Pair a b
dup f g x = Pair (f x) (g x)
tup :: a -> b -> Pair a b
tup a b = dup (const a) (const b) undefined
instance (Equal a, Equal b) => Equal (Pair a b) where
eq a b = and (eq (fst a) (fst b)) (eq (snd a) (snd b))
instance (Arbitrary a, Arbitrary b) => Arbitrary (Pair a b) where
arbitrary = do
a <- arbitrary
b <- arbitrary
return (Pair a b)
instance (CoArbitrary a, CoArbitrary b) => CoArbitrary (Pair a b) where
coarbitrary (Pair a b) = coarbitrary a . coarbitrary b
instance (TypeName a, TypeName b) => TypeName (Pair a b) where
typeName (Pair a b) = "Pair " ++ typeName a ++ " " ++ typeName b\(\dup\) is a \(\tup\).
Let \(A\) and \(B\) be sets. For all \(x \in A \times B\) we have \[\dup(f,g)(x) = \tup(f(x))(g(x)).\]
We have \[\begin{eqnarray*} & & \fst(\dup(f,g)(x)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-fst-dup} = & f(x) \end{eqnarray*}\] and \[\begin{eqnarray*} & & \snd(\dup(f,g)(x)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-snd-dup} = & g(x) \end{eqnarray*}\] so that \(\dup(f,g)(x) = \tup(f(x))(g(x))\) by the uniqueness of \(\tup\). as claimed.
For example, \(\id_{A \times B}\) is a \(\dup\).
Provided the types match up, we have \[\dup(\fst,\snd) = \id_{A \times B}.\]
Note that \[\begin{eqnarray*} & & \fst(\dup(\fst,\snd)(\tup(a)(b))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-fst-dup} = & \fst(\tup(a)(b)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-fst-tup} = & a \end{eqnarray*}\] and \[\begin{eqnarray*} & & \snd(\dup(\fst,\snd)(\tup(a)(b))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-snd-dup} = & \snd(\tup(a)(b)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & b \end{eqnarray*}\] so that \(\dup(\fst,\snd)(\tup(a)(b)) = \tup(a)(b)\) for all \(a \in A\) and \(b \in B\).
We define \(\tSwap\) on tuples like so.
Let \(A\) and \(B\) be sets. We define \(\tSwap : A \times B \rightarrow B \times A\) by \[\tSwap = \dup(\snd,\fst).\]
In Haskell,
Elements of \(A \times B\) act like “ordered pairs”, and \(\tSwap\) effectively reverses the order of the pair.
Let \(A\) and \(B\) be sets. Then we have the following.
- \(\tSwap(\tup(a)(b)) = \tup(b)(a)\).
- \(\tSwap(\tSwap(\tup(a)(b))) = \tup(a)(b)\).
- Note that \[\begin{eqnarray*} & & \fst(\tSwap(\tup(a)(b))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-tSwap} = & \fst(\dup(\snd,\fst)(\tup(a)(b))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-fst-dup} = & \snd(\tup(a)(b)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & b \end{eqnarray*}\] and \[\begin{eqnarray*} & & \snd(\tSwap(\tup(a)(b))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-tSwap} = & \snd(\dup(\snd,\fst)(\tup(a)(b))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-snd-dup} = & \fst(\tup(a)(b)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-fst-tup} = & a \end{eqnarray*}\] so that \(\tSwap(\tup(a)(b)) = \tup(b)(a)\) as claimed.
- Note that \[\begin{eqnarray*} & & \tSwap(\tSwap(\tup(a)(b))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-tSwap-swap} = & \tSwap(\tup(b)(a)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-tSwap-swap} = & \tup(a)(b) \end{eqnarray*}\] as claimed.
_test_tswap_entries :: (Equal a, Equal b)
=> a -> b -> Test (Pair a b -> Bool)
_test_tswap_entries _ _ =
testName "tswap(tup(a)(b)) == tup(b)(a)" $
\(Pair a b) -> eq (tswap (tup a b)) (tup b a)
_test_tswap_tswap :: (Equal a, Equal b)
=> a -> b -> Test (Pair a b -> Bool)
_test_tswap_tswap _ _ =
testName "tswap(tswap(x)) == x" $
\x -> eq (tswap (tswap x)) xNext, the utility \(\tPair\) facilitates defining functions from one tuple to another.
Let \(A\), \(B\), \(U\), and \(V\) be sets. We define \(\tPair : U^A \times V^B \rightarrow (U \times V)^{A \times B}\) by \[\tPair(f,g) = \dup(\compose(f)(\fst),\compose(g)(\snd)).\]
In Haskell:
\(\tPair\) has some nice properties.
For all \(f\), \(g\), \(h\), \(k\), \(a\), and \(b\) we have the following.
- \(\tPair(f,g)(\tup(a)(b)) = \tup(f(a))(g(b))\).
- \(\compose(\tPair(f,g))(\tPair(h,k)) = \tPair(\compose(f)(h),\compose(g)(k))\).
- Note that \[\begin{eqnarray*} & & \tPair(f,g)(\tup(a)(b)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-tPair} = & \dup(\compose(f)(\fst))(\compose(g)(\snd))(\tup(a)(b)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-dup-tup} = & \tup(\compose(f)(\fst)(\tup(a)(b)))(\compose(g)(\snd)(\tup(a)(b))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \tup(f(\fst(\tup(a)(b))))(\compose(g)(\snd)(\tup(a)(b))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \tup(f(\fst(\tup(a)(b))))(g(\snd(\tup(a)(b)))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-fst-tup} = & \tup(f(a))(g(\snd(\tup(a)(b)))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \tup(f(a))(g(b)) \end{eqnarray*}\] as claimed.
- Note that \[\begin{eqnarray*} & & \compose(\tPair(f,g))(\tPair(h,k))(\tup(a)(b)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \tPair(f,g)(\tPair(h,k)(\tup(a)(b))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-tPair-tup} = & \tPair(f,g)(\tup(h(a))(k(b))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-tPair-tup} = & \tup(f(h(a)))(g(k(b))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \tup(f(h(a)))(\compose(g)(k)(b)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \tup(\compose(f)(h)(a))(\compose(g)(k)(b)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-tPair-tup} = & \tPair(\compose(f)(h),\compose(g)(k))(\tup(a)(b)) \end{eqnarray*}\] as claimed.
_test_tpair_apply :: (Equal a, Equal b)
=> a -> b -> Test ((a -> a) -> (b -> b) -> Pair a b -> Bool)
_test_tpair_apply _ _ =
testName "tpair(f,g)(tup(a)(b)) == tup(f(a))(g(b))" $
\f g (Pair a b) -> eq (tpair f g (tup a b)) (tup (f a) (g b))
_test_tpair_tpair :: (Equal a, Equal b)
=> a -> b
-> Test ((a -> a) -> (b -> b) -> (a -> a) -> (b -> b) -> Pair a b -> Bool)
_test_tpair_tpair _ _ =
testName "tpair(f,g) . tpair(h,k) == tpair(f . h, g . k)" $
\f g h k x ->
eq
(tpair f g (tpair h k x))
(tpair (compose f h) (compose g k) x)Finally, note that although as sets \(A \times (B \times C)\) and \((A \times B) \times C\) cannot possibly be equal to each other in general, they are naturally isomorphic via \(\tAssocL\) and \(\tAssocR\).
Let \(A\), \(B\), and \(C\) be sets. We define \(\tAssocL : A \times (B \times C) \rightarrow (A \times B) \times C\) by \[\tAssocL = \dup(\dup(\fst,\compose(\fst)(\snd)),\compose(\snd)(\snd))\] and define \(\tAssocR : (A \times B) \times C \rightarrow A \times (B \times C)\) by \[\tAssocR = \dup(\compose(\fst)(\fst),\dup(\compose(\snd)(\fst),\snd)).\]
In Haskell:
Now \(\tAssocL\) and \(\tAssocR\) have some nice properties.
The following hold whenever everything has the appropriate type.
- \(\tAssocL(\tup(a)(\tup(b)(c))) = \tup(\tup(a)(b))(c)\).
- \(\tAssocR(\tup(\tup(a)(b))(c)) = \tup(a)(\tup(b)(c))\).
- \(\compose(\tAssocR)(\tAssocL) = \id\).
- \(\compose(\tAssocL)(\tAssocR) = \id\).
- Note that \[\begin{eqnarray*} & & \tAssocL(\tup(a)(\tup(b)(c))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-tAssocL} = & \dup(\dup(\fst,\compose(\fst)(\snd)),\compose(\snd)(\snd))(\tup(a)(\tup(b)(c))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-dup-tup} = & \tup(\dup(\fst,\compose(\fst)(\snd))(\tup(a)(\tup(b)(c))))(\compose(\snd)(\snd)(\tup(a)(\tup(b)(c)))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \tup(\dup(\fst,\compose(\fst)(\snd))(\tup(a)(\tup(b)(c))))(\snd(\snd(\tup(a)(\tup(b)(c))))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \tup(\dup(\fst,\compose(\fst)(\snd))(\tup(a)(\tup(b)(c))))(\snd(\tup(b)(c))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \tup(\dup(\fst,\compose(\fst)(\snd))(\tup(a)(\tup(b)(c))))(c) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-dup-tup} = & \tup(\tup(\fst(\tup(a)(\tup(b)(c))))(\compose(\fst)(\snd)(\tup(a)(\tup(b)(c)))))(c) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \tup(\tup(\fst(\tup(a)(\tup(b)(c))))(\fst(\snd(\tup(a)(\tup(b)(c))))))(c) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \tup(\tup(\fst(\tup(a)(\tup(b)(c))))(\fst(\tup(b)(c))))(c) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-fst-tup} = & \tup(\tup(\fst(\tup(a)(\tup(b)(c))))(b))(c) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-fst-tup} = & \tup(\tup(a)(b))(c) \end{eqnarray*}\] as claimed.
- Note that \[\begin{eqnarray*} & & \tAssocR(\tup(\tup(a)(b))(c)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-tAssocR} = & \dup(\compose(\fst)(\fst),\dup(\compose(\snd)(\fst),\snd))(\tup(\tup(a)(b))(c)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-dup-tup} = & \tup(\compose(\fst)(\fst)(\tup(\tup(a)(b))(c)))(\dup(\compose(\snd)(\fst),\snd)(\tup(\tup(a)(b))(c))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \tup(\fst(\fst(\tup(\tup(a)(b))(c))))(\dup(\compose(\snd)(\fst),\snd)(\tup(\tup(a)(b))(c))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-fst-tup} = & \tup(\fst(\tup(a)(b)))(\dup(\compose(\snd)(\fst),\snd)(\tup(\tup(a)(b))(c))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-fst-tup} = & \tup(a)(\dup(\compose(\snd)(\fst),\snd)(\tup(\tup(a)(b))(c))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-dup-tup} = & \tup(a)(\tup(\compose(\snd)(\fst)(\tup(\tup(a)(b))(c)))(\snd(\tup(\tup(a)(b))(c)))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \tup(a)(\tup(\compose(\snd)(\fst)(\tup(\tup(a)(b))(c)))(c)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \tup(a)(\tup(\snd(\fst(\tup(\tup(a)(b))(c))))(c)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-fst-tup} = & \tup(a)(\tup(\snd(\tup(a)(b)))(c)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \tup(a)(\tup(b)(c)) \end{eqnarray*}\] as claimed.
- Note that \[\begin{eqnarray*} & & \compose(\tAssocR)(\tAssocL)(\tup(a)(\tup(b)(c))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \tAssocR(\tAssocL(\tup(a)(\tup(b)(c)))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-tAssocL-tup} = & \tAssocR(\tup(\tup(a)(b))(c)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-tAssocR-tup} = & \tup(a)(\tup(b)(c)) \end{eqnarray*}\] as claimed.
- Note that \[\begin{eqnarray*} & & \compose(\tAssocL)(\tAssocR)(\tup(\tup(a)(b))(c)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \tAssocL(\tAssocR(\tup(\tup(a)(b))(c))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-tAssocR-tup} = & \tAssocL(\tup(a)(\tup(b)(c))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-tAssocL-tup} = & \tup(\tup(a)(b))(c) \end{eqnarray*}\] as claimed.
_test_tassocL_entries :: (Equal a, Equal b, Equal c)
=> a -> b -> c -> Test (a -> b -> c -> Bool)
_test_tassocL_entries _ _ _ =
testName "tassocL(tup(a)(tup(b)(c))) == tup(tup(a)(b))(c)" $
\a b c -> eq (tassocL (tup a (tup b c))) (tup (tup a b) c)
_test_tassocR_entries :: (Equal a, Equal b, Equal c)
=> a -> b -> c -> Test (a -> b -> c -> Bool)
_test_tassocR_entries _ _ _ =
testName "tassocR(tup(tup(a)(b))(c)) == tup(a)(tup(b)(c))" $
\a b c -> eq (tassocR (tup (tup a b) c)) (tup a (tup b c))
_test_tassocL_tassocR :: (Equal a, Equal b, Equal c)
=> a -> b -> c -> Test (Pair (Pair a b) c -> Bool)
_test_tassocL_tassocR _ _ _ =
testName "compose(tassocL)(tassocR) == id" $
\x -> eq (tassocL (tassocR x)) x
_test_tassocR_tassocL :: (Equal a, Equal b, Equal c)
=> a -> b -> c -> Test (Pair a (Pair b c) -> Bool)
_test_tassocR_tassocL _ _ _ =
testName "compare(tassocR)(tassocL) == id" $
\x -> eq (tassocR (tassocL x)) xHigher-order functions can be converted to functions on tuples (and back).
Let \(A\), \(B\), and \(C\) be sets. If \(f : A \rightarrow B \rightarrow C\), we define \(\uncurry(f) : A \times B \rightarrow C\) by \[\uncurry(f)(\tup(a)(b)) = f(a)(b).\] If \(g : A \times B \rightarrow C\), we define \(\curry(g) : A \rightarrow B \rightarrow C\) by \[\curry(g)(a)(b) = g(\tup(a)(b)).\]
In Haskell:
Testing
Suite:
_test_tuple
:: ( 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
) => Int -> Int -> a -> b -> c -> IO ()
_test_tuple size cases a b c = do
testLabel3 "Tuple" a b c
let args = testArgs size cases
runTest args (_test_dup_fst_snd a b)
runTest args (_test_dup_tup a b)
runTest args (_test_tswap_entries a b)
runTest args (_test_tswap_tswap a b)
runTest args (_test_tpair_apply a b)
runTest args (_test_tpair_tpair a b)
runTest args (_test_tassocL_entries a b c)
runTest args (_test_tassocR_entries a b c)
runTest args (_test_tassocL_tassocR a b c)
runTest args (_test_tassocR_tassocL a b c)Main: