Unzip

Posted on 2017-05-07 by nbloomf

Tags: arithmetic-made-difficult, literate-haskell

\(\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 #-}
module Unzip
  ( unzip, _test_unzip, main_unzip
  ) where

import Testing
import Booleans
import Tuples
import NaturalNumbers
import Lists
import Map
import Zip

Today we will define a kind of one-sided inverse of \(\zip\), called \(\unzip\). Recall that \(\zip\) has signature \[\lists{A} \times \lists{B} \rightarrow \lists{A \times B}.\] An inverse will then have signature \[\lists{A \times B} \rightarrow \lists{A} \times \lists{B},\] and should “undo” the zipping. As usual we’d like to define this as a fold if possible; to that end we need \(\varepsilon : \lists{A} \times \lists{B}\) and \[\varphi : (A \times B) \times (\lists{A} \times \lists{B}) \rightarrow \lists{A} \times \lists{B}\] such that \[\begin{eqnarray*} & & (\nil,\nil) \\ & = & \unzip(\nil) \\ & = & \foldr(\varepsilon)(\varphi)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \varepsilon \end{eqnarray*}\] and if \(\unzip(x) = (u,v)\), then \[\begin{eqnarray*} & & (\cons(a,u),\cons(b,v)) \\ & = & \unzip(\cons((a,b),x)) \\ & = & \foldr(\varepsilon)(\varphi)(\cons((a,b),x)) \\ & = & \varphi((a,b),\foldr(\varepsilon)(\varphi)(x)) \\ & = & \varphi((a,b),\unzip(x)) \\ & = & \varphi((a,b),(u,v)). \end{eqnarray*}\] With this in mind, we define \(\unzip\) like so.

Let \(A\) and \(B\) be sets. Define \(\varphi : (A \times B) \times (\lists{A} \times \lists{B}) \rightarrow \lists{A} \times \lists{B}\) by \[\varphi(u,z) = \tup(\cons(\fst(u),\fst(z)),\cons(\snd(u),\snd(z))).\] We then define \(\unzip : \lists{A \times B} \rightarrow \lists{A} \times \lists{B}\) by \[\unzip = \foldr(\tup(\nil)(\nil))(\varphi).\]

In Haskell:

unzip :: (List t) => t (Pair a b) -> Pair (t a) (t b)
unzip = foldr (tup nil nil) phi
  where
    phi u z = tup (cons (fst u) (fst z)) (cons (snd u) (snd z))

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

Let \(A\) and \(B\) be sets. Then \(\unzip\) is the unique map \(f : \lists{A \times B} \rightarrow \lists{A} \times \lists{B}\) such that the following hold for all \(a \in A\), \(b \in B\), \(x \in \lists{A}\), and \(y \in \lists{B}\). \[\left\{\begin{array}{l} f(\nil) = \tup(\nil)(\nil) \\ f(\cons(u,z)) = \tup(\cons(\fst(u),\fst(z)))(\cons(\snd(u),\snd(z))). \end{array}\right.\]

_test_unzip_nil :: (List t, Equal (t a), Equal (t b))
  => t a -> t b -> Test Bool
_test_unzip_nil ta tb =
  testName "unzip(nil) == (nil,nil)" $
  eq (unzip nil) (tup (nil `withTypeOf` ta) (nil `withTypeOf` tb))


_test_unzip_cons :: (List t, Equal (t a), Equal (t b))
  => t a -> t b -> Test (a -> b -> t (Pair a b) -> Bool)
_test_unzip_cons ta tb =
  testName "unzip(cons((a,b),z)) == (cons(a,fst(unzip(z))),cons(b,snd(unzip(z))))" $
  \a b z -> eq
    (unzip (cons (tup a b) z))
    (tup (cons a (fst (unzip z))) (cons b (snd (unzip z))))

Now \(\zip\) undoes \(\unzip\) as expected.

Let \(A\) and \(B\) be sets. For all \(x \in \lists{A \times B}\), we have \[\uncurry(\zip)(\unzip(x)) = x.\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \uncurry(\zip)(\unzip(x)) \\ & \hyp{x = \nil} = & \uncurry(\zip)(\unzip(\nil)) \\ & = & \uncurry(\zip)(\tup(\nil)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#def-uncurry} = & \zip(\nil)(\nil) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-nil-left} = & \nil \\ & \hyp{x = \nil} = & x \end{eqnarray*}\] as needed. Suppose now that the result holds for some \(x\) and let \(a \in A\) and \(b \in B\). Let \((u,v) = \unzip(x)\). Now \[\begin{eqnarray*} & & \uncurry(\zip)(\unzip(\cons(\tup(a)(b),x))) \\ & = & \uncurry(\zip)\tup(\cons(a,\fst(\unzip(x))))(\cons(b,\snd(\unzip(x)))) \\ & = & \zip(\cons(a,\fst(\unzip(x))))(\cons(b,\snd(\unzip(x)))) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-cons-cons} = & \cons(\tup(a)(b),\zip(\fst(\unzip(x)),\snd(\unzip(x)))) \\ & = & \cons(\tup(a)(b),\uncurry(\zip)(\unzip(x))) \\ & \hyp{\uncurry(\zip)(\unzip(x)) = x} = & \cons(\tup(a)(b),x) \end{eqnarray*}\] as needed.

_test_unzip_zip :: (List t, Equal a, Equal b, Equal (t (Pair a b)))
  => t a -> t b -> Test (t (Pair a b) -> Bool)
_test_unzip_zip _ _ =
  testName "zip(unzip(x)) == x" $
  \x -> eq ((uncurry zip) (unzip x)) x

(Note that the reverse composition \(\unzip(\zip(x,y)) = (x,y),\) although it makes sense type-wise, does not hold for all \(x\) and \(y\) since \(\zip\) truncates its longer argument.)

\(\unzip\) interacts with \(\tSwap\):

Let \(A\) and \(B\) be sets and \(x \in \lists{A \times B}\). Then we have \[\tSwap(\unzip(x)) = \unzip(\map(\tSwap)(x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \tSwap(\unzip(x)) \\ & \hyp{x = \nil} = & \tSwap(\unzip(\nil)) \\ & = & \tSwap(\nil,\nil) \\ & = & (\nil,\nil) \\ & = & \unzip(\nil) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \unzip(\map(\tSwap)(\nil)) \\ & \hyp{x = \nil} = & \unzip(\map(\tSwap)(x)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\), and let \((a,b) \in A \times B\). Suppose \((u,v) = \unzip(x)\); by the inductive hypothesis we have \((v,u) = \unzip(\map(\tSwap)(x))\). Now \[\begin{eqnarray*} & & \unzip(\map(\tSwap)(\cons((a,b),x))) \\ & = & \unzip(\cons(\tSwap(a,b),\map(\tSwap)(x))) \\ & = & \unzip(\cons((b,a),\map(\tSwap)(x))) \\ & = & (\cons(b,v),\cons(a,u)) \\ & = & \tSwap(\cons(a,u),\cons(b,v)) \\ & = & \tSwap(\unzip(\cons((a,b),x))) \end{eqnarray*}\] as claimed.

_test_unzip_tswap :: (List t, Equal (t b), Equal (t a))
  => t a -> t b -> Test (t (Pair a b) -> Bool)
_test_unzip_tswap _ _ =
  testName "tswap(unzip(x)) == unzip(map(tswap)(x))" $
  \x -> eq (unzip (map tswap x)) (tswap (unzip x))

\(\unzip\) interacts with \(\tPair\).

Let \(A\), \(B\), \(U\), and \(V\) be sets, with \(f : A \rightarrow U\) and \(g : B \rightarrow V\). For all \(x \in \lists{A \times B}\) we have \[\unzip(\map(\tPair(f,g))(x)) = \tPair(\map(f),\map(g))(\unzip(x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \unzip(\map(\tPair(f,g))(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \unzip(\nil) \\ & = & \tup(\nil)(\nil) \\ & = & \tup(\map(f)(\nil))(\map(g)(\nil)) \\ & = & \tPair(\map(f),\map(g))(\nil,\nil) \\ & = & \tPair(\map(f),\map(g))(\unzip(\nil)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \((a,b) \in A \times B\). Say \((u,v) = \unzip(x)\). Letting \(\varphi\) be as in the definition of \(\unzip\) and using the inductive hypothesis, we have \[\begin{eqnarray*} & & \tPair(\map(f),\map(g))(\unzip(\cons((a,b),x))) \\ & = & \tPair(\map(f),\map(g))(\cons(a,u),\cons(b,v)) \\ & = & (\map(f)(\cons(a,u)),\map(g)(\cons(b,v))) \\ & = & (\cons(f(a),\map(f)(u)),\cons(g(b),\map(g)(v))) \\ & = & \varphi((f(a),g(b)),(\map(f)(u),\map(g)(v))) \\ & = & \varphi((f(a),g(b)),\tPair(\map(f),\map(g))(u,v)) \\ & = & \varphi((f(a),g(b)),\tPair(\map(f),\map(g))(\unzip(x))) \\ & = & \varphi((f(a),g(b)),\unzip(\map(\tPair(f,g))(x))) \\ & = & \varphi(\tPair(f,g)(a,b),\unzip(\map(\tPair(f,g))(x))) \\ & = & \varphi(\tPair(f,g)(a,b),\foldr((\nil,\nil))(\varphi)(\map(\tPair(f,g))(x))) \\ & = & \foldr((\nil,\nil))(\varphi)(\cons(\tPair(f,g)(a,b),\map(\tPair(f,g))(x))) \\ & = & \foldr((\nil,\nil))(\varphi)(\map(\tPair(f,g))(\cons((a,b),x))) \\ & = & \unzip(\map(\tPair(f,g))(\cons((a,b),x))) \end{eqnarray*}\] as needed.

_test_unzip_tpair :: (List t, Equal (t b), Equal (t a))
  => t a -> t b -> Test ((a -> a) -> (b -> b) -> t (Pair a b) -> Bool)
_test_unzip_tpair _ _ =
  testName "unzip(map(tpair(f,g))(x)) == tpair(map(f),map(g))(unzip(x))" $
  \f g x -> eq (unzip (map (tpair f g) x)) (tpair (map f) (map g) (unzip x))

Testing

Suite:

_test_unzip ::
  ( TypeName a, Show a, Equal a, Arbitrary a, CoArbitrary a
  , TypeName b, Show b, Equal b, Arbitrary b, CoArbitrary b
  , TypeName (t a), TypeName (t b), List t
  , Equal (t (Pair a b)), Arbitrary (t a), Show (t a), Arbitrary (t b), Show (t b)
  , Show (t (Pair a b)), Arbitrary (t (Pair a b)), Equal (t b), Equal (t a)
  ) => Int -> Int -> t a -> t b -> IO ()
_test_unzip size cases t u = do
  testLabel2 "unzip" t u

  let args = testArgs size cases

  runTest args (_test_unzip_nil t u)
  runTest args (_test_unzip_cons t u)
  runTest args (_test_unzip_zip t u)
  runTest args (_test_unzip_tswap t u)
  runTest args (_test_unzip_tpair t u)

Main:

main_unzip :: IO ()
main_unzip = do
  _test_unzip 20 100 (nil :: ConsList Bool)  (nil :: ConsList Bool)
  _test_unzip 20 100 (nil :: ConsList Unary) (nil :: ConsList Unary)