Disjoint Unions

Posted on 2017-12-21 by nbloomf

Tags: literate-haskell, arithmetic-made-difficult

\(\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, ScopedTypeVariables #-}
module DisjointUnions
  ( Union(..), lft, rgt, either, uswap, upair , uassocL, uassocR, isLft, isRgt
  , _test_disjoint_union, main_disjoint_union
  ) where

import Testing
import Functions
import Flip
import Clone
import Composition
import Booleans

Dual to sets of tuples are disjoint sums.

Let \(A\) and \(B\) be sets. There is a set \(A + B\) together with two functions \(\lft : A \rightarrow A + B\) and \(\rgt : B \rightarrow A + B\) having the property that if \(X\) is a set and \(\sigma : A \rightarrow X\) and \(\tau : B \rightarrow X\) functions then there is a unique map \(\Theta : A + B \rightarrow X\) such that \(\Theta \circ \lft = \sigma\) and \(\Theta \circ \rgt = \tau\). That is, there is a unique \(\Theta\) such that the following diagram commutes.

\[\require{AMScd} \begin{CD} A @>{\lft}>> A + B @<{\rgt}<< B \\ @V{\sigma}VV @VV{\Theta}V @VV{\tau}V \\ X @= X @= X \end{CD}\]

We will denote this unique \(\Theta : A + B \rightarrow X\) by \(\either(\sigma,\tau)\).

More concretely, if \(f : A + B \rightarrow X\) such that \(f(\lft(a)) = \sigma(a)\) and \(f(\rgt(b)) = \tau(b)\) for all \(a \in A\) and \(b \in B\), then \(f = \either(\sigma,\tau)\).

Now every element of \(A+B\) is uniquely either of the form \(\lft(a)\) or \(\rgt(b)\) for some \(a \in A\) or \(b \in B\); this allows us to use case analysis on \(A + B\). This set is sometimes called a tagged union, because it behaves like an ordinary set-theoretic union where elements are “tagged” with the set they came from (so, for instance, if \(x \in A\) and \(x \in B\), the \(x\) from \(A\) and the \(x\) from \(B\) are distinct in \(A+B\)).

Let \(A\) and \(B\) be sets.

If \(x \in A + B\), then either \(x = \lft(a)\) for some \(a \in A\) or \(x = \rgt(b)\) for some \(b \in B\).
There does not exist \(x \in A + B\) such that \(x = \lft(a)\) and \(x = \rgt(b)\) for some \(a \in A\) and \(b \in B\).
\(\lft : A \rightarrow A+B\) and \(\rgt : B \rightarrow A+B\) are injective.

Suppose to the contrary that there exists some \(z \in A+B\) which is not of the form \(\lft(a)\) or \(\rgt(b)\) for any \(a\) or \(b\). Now consider \[f = \const(\btrue)\] and \[g(x) = \bif{\beq(x,z)}{\bfalse}{\btrue}\] as functions \(A+B \rightarrow \bool\). Note in particular that if \(a \in A\) we have \[\begin{eqnarray*} & & \compose(f)(\lft)(a) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & f(\lft(a)) \\ & \let{f = \const(\btrue)} = & \const(\btrue)(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \btrue \\ & \hyp{g(\lft(a)) = \btrue} = & g(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \compose(g)(\lft)(a) \end{eqnarray*}\] since \(z \neq \lft(a)\), and if \(b \in B\) we have \[\begin{eqnarray*} & & \compose(f)(\rgt)(b) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & f(\rgt(b)) \\ & \let{f = \const(\btrue)} = & \const(\btrue)(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \btrue \\ & \hyp{g(\rgt(b)) = \btrue} = & g(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \compose(g)(\rgt)(b) \end{eqnarray*}\] similarly. By the universal property of \(A + B\), we thus have \[f = \either(\const(\btrue),\const(\btrue)) = g.\] But now we have \[\btrue = f(z) = g(z) = \bfalse,\] which is absurd.
Suppose to the contrary that we have \(z \in A + B\) with \(\lft(a) = z = \rgt(b)\) for some \(a \in A\) and \(b \in B\), and consider now \(f : A+B \rightarrow \bool\) given by \[f = \either(\const(\btrue),\const(\bfalse)).\] We then have \[\begin{eqnarray*} & & \btrue \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \const(\btrue)(a) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \either(\const(\btrue),\const(\bfalse))(\lft(a)) \\ & \let{z = \lft(a)} = & \either(\const(\btrue),\const(\bfalse))(z) \\ & \let{z = \rgt(b)} = & \either(\const(\btrue),\const(\bfalse))(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \const(\bfalse)(b) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \bfalse \end{eqnarray*}\] which is absurd.
Let \(u,v \in A\), and suppose \(\lft(u) = \lft(v)\). Now define \(f : A \rightarrow \bool\) by \[f(x) = \bif{\beq(x,u)}{\bfalse}{\btrue},\] and consider \(g = \either(f,\const(\btrue))\). We have \[\begin{eqnarray*} & & \bfalse \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{\bfalse}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \bif{\beq(u,u)}{\bfalse}{\btrue} \\ & \let{f(x) = \bif{\beq(x,u)}{\bfalse}{\btrue}} = & f(u) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \either(f,\const(\btrue))(\lft(u)) \\ & \hyp{\lft(u) = \lft(v)} = & \either(f,\const(\btrue))(\lft(v)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & f(v) \\ & \let{f(x) = \bif{\beq(x,u)}{\bfalse}{\btrue}} = & \bif{\beq(v,u)}{\bfalse}{\btrue} \end{eqnarray*}\] thus \(v = u\) as needed. A similar argument holds for \(\rgt\).

The previous results suggest that we can model \(A + B\) with the Haskell type Either a b. For simplicity’s sake we’ll redefine this type, and the maps in the universal property, like so.

data Union a b
  = Left a | Right b
  deriving Show

lft :: a -> Union a b
lft a = Left a

rgt :: b -> Union a b
rgt b = Right b

either :: (a -> x) -> (b -> x) -> Union a b -> x
either f _ (Left  a) = f a
either _ g (Right b) = g b

instance (Equal a, Equal b) => Equal (Union a b) where
  eq (Left a1)  (Left a2)  = eq a1 a2
  eq (Left _)   (Right _)  = false
  eq (Right _)  (Left _)   = false
  eq (Right b1) (Right b2) = eq b1 b2

instance (Arbitrary a, Arbitrary b) => Arbitrary (Union a b) where
  arbitrary = do
    s <- arbitrary
    if s
      then arbitrary >>= (return . Left)
      else arbitrary >>= (return . Right)

instance (CoArbitrary a, CoArbitrary b) => CoArbitrary (Union a b) where
  coarbitrary (Left  a) = variant (0 :: Int) . coarbitrary a
  coarbitrary (Right b) = variant (1 :: Int) . coarbitrary b

instance (TypeName a, TypeName b) => TypeName (Union a b) where
  typeName _ =
    "Union " ++ typeName (undefined :: a) ++ " " ++ typeName (undefined :: b)

For example, \(\id_{A + B}\) is an \(\either\).

Provided the types match up, we have \[\either(\lft,\rgt) = \id_{A + B}.\]

If \(a \in A\), we have \[\begin{eqnarray*} & & \compose(\id)(\lft)(a) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \id(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-id} = & \lft(a) \end{eqnarray*}\] and likewise if \(b \in B\) we have \[\begin{eqnarray*} & & \compose(\id)(\rgt)(b) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \id(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-id} = & \rgt(b) \end{eqnarray*}\] Since \(\either(\lft,\rgt)\) is unique with this property, we have \(\either(\lft,\rgt) = \id_{A+B}\) as claimed.

_test_either_lft_rgt :: (Equal a, Equal b)
  => a -> b -> Test (Union a b -> Bool)
_test_either_lft_rgt _ _ =
  testName "either(lft,rgt) == id" $
  \x -> eq (either lft rgt x) x

We define \(\uSwap\) on disjoint unions like so.

Let \(A\) and \(B\) be sets. We define \(\uSwap : A + B \rightarrow B + A\) by \[\uSwap = \either(\rgt,\lft).\]

In Haskell:

uswap :: Union a b -> Union b a
uswap = either rgt lft

Now \(\uSwap\) effectively toggles the tag of its argument.

Let \(A\) and \(B\) be sets. Then we have the following for all \(a \in A\) and \(b \in B\).

\(\uSwap(\lft(a)) = \rgt(a)\).
\(\uSwap(\rgt(b)) = \lft(b)\).
\(\compose(\uSwap)(\uSwap) = \id\).

Note that \[\begin{eqnarray*} & & \uSwap(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-uSwap} = & \either(\rgt,\lft)(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \rgt(a) \end{eqnarray*}\] as claimed.
Note that \[\begin{eqnarray*} & & \uSwap(\rgt(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-uSwap} = & \either(\rgt,\lft)(\rgt(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \lft(a) \end{eqnarray*}\] as claimed.
Let \(x \in A+B\); we have two possibilities. If \(x = \lft(a)\), we have \[\begin{eqnarray*} & & \compose(\uSwap)(\uSwap)(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \uSwap(\uSwap(\lft(a))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uSwap-lft} = & \uSwap(\rgt(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uSwap-rgt} = & \lft(a) \end{eqnarray*}\] and if \(x = \rgt(b)\) we have \[\begin{eqnarray*} & & \compose(\uSwap)(\uSwap)(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \uSwap(\uSwap(\rgt(b))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uSwap-rgt} = & \uSwap(\lft(b)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uSwap-lft} = & \rgt(b) \end{eqnarray*}\] as needed.

_test_uswap_lft :: (Equal a, Equal b)
  => a -> b -> Test (a -> Bool)
_test_uswap_lft _ y =
  testName "uswap(left(a)) == right(a)" $
  \a -> eq
    (uswap (lft a))
    ((rgt a) `withTypeOf` (lft y))


_test_uswap_rgt :: (Equal a, Equal b)
  => a -> b -> Test (b -> Bool)
_test_uswap_rgt x _ =
  testName "uswap(right(a)) == left(a)" $
  \b -> eq
    (uswap (rgt b))
    ((lft b) `withTypeOf` (rgt x))


_test_uswap_uswap :: (Equal a, Equal b)
  => a -> b -> Test (Union a b -> Bool)
_test_uswap_uswap _ _ =
  testName "swap(swap(x)) == x" $
  \x -> eq (uswap (uswap x)) x

Next, the utility \(\uPair\) facilitates defining functions from one disjoint union to another.

Let \(A\), \(B\), \(U\), and \(V\) be sets. We define \(\uPair : U^A \times V^B \rightarrow (U + V)^{A + B}\) by \[\uPair(f,g) = \either(\compose(\lft)(f),\compose(\rgt)(g)).\]

In Haskell:

upair :: (a -> u) -> (b -> v) -> Union a b -> Union u v
upair f g = either (lft . f) (rgt . g)

\(\uPair\) has some nice properties.

For all \(f\), \(g\), \(h\), \(k\), \(a\), and \(b\) we have the following.

\(\uPair(f,g)(\lft(a)) = \lft(f(a))\).
\(\uPair(f,g)(\rgt(b)) = \rgt(g(b))\).
\(\compose(\uPair(f,g))(\uPair(h,k)) = \uPair(\compose(f)(h),\compose(g)(k))\).

Note that \[\begin{eqnarray*} & & \uPair(f,g)(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-uPair} = & \either(\compose(\lft)(f),\compose(\rgt)(g))(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \compose(\lft)(f)(a) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \lft(f(a)) \end{eqnarray*}\] as claimed.
Note that \[\begin{eqnarray*} & & \uPair(f,g)(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-uPair} = & \either(\compose(\lft)(f),\compose(\rgt)(g))(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \compose(\rgt)(g)(b) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \rgt(g(b)) \end{eqnarray*}\] as claimed.
We consider two possibilities: note that \[\begin{eqnarray*} & & \compose(\uPair(f,g))(\uPair(h,k))(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \uPair(f,g)(\uPair(h,k)(\lft(a))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uPair-lft} = & \uPair(f,g)(\lft(h(a))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uPair-lft} = & \lft(f(h(a))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \lft(\compose(f)(h)(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uPair-lft} = & \uPair(\compose(f)(h),\compose(g)(k))(\lft(a)) \end{eqnarray*}\] and \[\begin{eqnarray*} & & \compose(\uPair(f,g))(\uPair(h,k))(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \uPair(f,g)(\uPair(h,k)(\rgt(b))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uPair-rgt} = & \uPair(f,g)(\rgt(k(b))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uPair-rgt} = & \rgt(g(k(b))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \rgt(\compose(g)(k)(b)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uPair-rgt} = & \uPair(\compose(f)(h),\compose(g)(k))(\rgt(b)) \end{eqnarray*}\] as needed.

_test_upair_lft :: (Equal a, Equal b)
  => a -> b -> Test ((a -> a) -> (b -> b) -> a -> Bool)
_test_upair_lft _ y =
  testName "upair(f,g)(lft(a)) == lft(f(a))" $
  \f g a -> eq
    (upair f g ((lft a) `withTypeOf` (rgt y)))
    ((lft (f a)) `withTypeOf` (rgt y))


_test_upair_rgt :: (Equal a, Equal b)
  => a -> b -> Test ((a -> a) -> (b -> b) -> b -> Bool)
_test_upair_rgt x _ =
  testName "upair(f,g)(rgt(b)) == rgt(g(b))" $
  \f g b -> eq
    (upair f g ((rgt b) `withTypeOf` (lft x)))
    ((rgt (g b)) `withTypeOf` (lft x))


_test_upair_upair :: (Equal a, Equal b)
  => a -> b
  -> Test ((a -> a) -> (b -> b) -> (a -> a) -> (b -> b)
      -> Union a b -> Bool)
_test_upair_upair _ _ =
  testName "upair(f,g) . upair(h,k) == upair(f . h, g . k)" $
  \f g h k x ->
    eq
      (upair f g (upair h k x))
      (upair (f . h) (g . k) x)

Finally, note that although as sets \(A + (B + C)\) and \((A + B) + C\) cannot possibly be equal to each other in general, they are naturally isomorphic via \(\uAssocL\) and \(\uAssocR\).

Let \(A\), \(B\), and \(C\) be sets. We define \(\uAssocL : A + (B + C) \rightarrow (A + B) + C\) by \[\uAssocL = \either(\compose(\lft)(\lft),\either(\compose(\lft)(\rgt),\rgt))\] and define \(\uAssocR : (A + B) + C \rightarrow A + (B + C)\) by \[\uAssocR = \either(\either(\lft,\compose(\rgt)(\lft)),\compose(\rgt)(\rgt)).\]

In Haskell:

uassocL :: Union a (Union b c) -> Union (Union a b) c
uassocL = either (lft . lft) (either (lft . rgt) rgt)

uassocR :: Union (Union a b) c -> Union a (Union b c)
uassocR = either (either lft (rgt . lft)) (rgt . rgt)

Now \(\uAssocL\) and \(\uAssocR\) have some nice properties.

The following hold whenever everything has the appropriate type.

\(\uAssocL(\lft(a)) = \lft(\lft(a))\).
\(\uAssocL(\rgt(\lft(b))) = \lft(\rgt(b))\).
\(\uAssocL(\rgt(\rgt(c))) = \rgt(c)\).
\(\uAssocR(\lft(\lft(a))) = \lft(a)\).
\(\uAssocR(\lft(\rgt(b))) = \rgt(\lft(b))\).
\(\uAssocR(\rgt(c)) = \rgt(\rgt(c))\).
\(\compose(\uAssocR)(\uAssocL) = \id_{A + (B + C)}\).
\(\compose(\uAssocL)(\uAssocR) = \id_{(A + B) + C}\).

We have \[\begin{eqnarray*} & & \uAssocL(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-uAssocL} = & \either(\compose(\lft)(\lft),\either(\compose(\lft)(\rgt),\rgt))(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \compose(\lft)(\lft)(a) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \lft(\lft(a)) \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \uAssocL(\rgt(\lft(b))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-uAssocL} = & \either(\compose(\lft)(\lft),\either(\compose(\lft)(\rgt),\rgt))(\rgt(\lft(b))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \either(\compose(\lft)(\rgt),\rgt)(\lft(b)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \compose(\lft)(\rgt)(b) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \lft(\rgt(b)) \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \uAssocL(\rgt(\rgt(c))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-uAssocL} = & \either(\compose(\lft)(\lft),\either(\compose(\lft)(\rgt),\rgt))(\rgt(\rgt(c))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \either(\compose(\lft)(\rgt),\rgt)(\rgt(c)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \rgt(c) \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \uAssocR(\lft(\lft(a))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-uAssocR} = & \either(\either(\lft,\compose(\rgt)(\lft)),\compose(\rgt)(\rgt))(\lft(\lft(a))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \either(\lft,\compose(\rgt)(\lft))(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \lft(a) \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \uAssocR(\lft(\rgt(b))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-uAssocR} = & \either(\either(\lft,\compose(\rgt)(\lft)),\compose(\rgt)(\rgt))(\lft(\rgt(b))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \either(\lft,\compose(\rgt)(\lft))(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \compose(\rgt)(\lft)(b) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \rgt(\lft(b)) \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \uAssocR(\rgt(c)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-uAssocR} = & \either(\either(\lft,\compose(\rgt)(\lft)),\compose(\rgt)(\rgt))(\rgt(c)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \compose(\rgt)(\rgt)(c) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \rgt(\rgt(c)) \end{eqnarray*}\] as claimed.
If \(x \in A + (B + C)\), we have three possibilities. If \(x = \lft(a)\), note that \[\begin{eqnarray*} & & \compose(\uAssocR)(\uAssocL)(x) \\ & \let{x = \lft(a)} = & \compose(\uAssocR)(\uAssocL)(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \uAssocR(\uAssocL(\lft(a))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uAssocL-lft} = & \uAssocR(\lft(\lft(a))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uAssocR-lft-lft} = & \lft(a) \\ & \let{x = \lft(a)} = & x \end{eqnarray*}\] if \(x = \rgt(\lft(b))\), note that \[\begin{eqnarray*} & & \compose(\uAssocR)(\uAssocL)(x) \\ & \let{x = \rgt(\lft(b))} = & \compose(\uAssocR)(\uAssocL)(\rgt(\lft(b))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \uAssocR(\uAssocL(\rgt(\lft(b)))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uAssocL-rgt-lft} = & \uAssocR(\lft(\rgt(b))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uAssocR-lft-rgt} = & \rgt(\lft(b)) \\ & \let{x = \rgt(\lft(b))} = & x \end{eqnarray*}\] and if \(x = \rgt(\rgt(c))\), note that \[\begin{eqnarray*} & & \compose(\uAssocR)(\uAssocL)(x) \\ & \let{x = \rgt(\rgt(c))} = & \compose(\uAssocR)(\uAssocL)(\rgt(\rgt(c))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \uAssocR(\uAssocL(\rgt(\rgt(c)))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uAssocL-rgt-rgt} = & \uAssocR(\rgt(c)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uAssocR-rgt} = & \rgt(\rgt(c)) \\ & \let{x = \rgt(\rgt(c))} = & x \end{eqnarray*}\] as needed.
If \(x \in (A + B) + C\), we have three possibilities. If \(x = \lft(\lft(a))\), note that \[\begin{eqnarray*} & & \compose(\uAssocL)(\uAssocR)(x) \\ & \let{x = \lft(\lft(a))} = & \compose(\uAssocL)(\uAssocR)(\lft(\lft(a))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \uAssocL(\uAssocR(\lft(\lft(a)))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uAssocR-lft-lft} = & \uAssocL(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uAssocL-lft} = & \lft(\lft(a)) \\ & \let{x = \lft(\lft(a))} = & x \end{eqnarray*}\] if \(x = \lft(\rgt(b))\), note that \[\begin{eqnarray*} & & \compose(\uAssocL)(\uAssocR)(x) \\ & \let{x = \lft(\rgt(b))} = & \compose(\uAssocL)(\uAssocR)(\lft(\rgt(b))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \uAssocL(\uAssocR(\lft(\rgt(b)))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uAssocR-lft-rgt} = & \uAssocL(\rgt(\lft(b))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uAssocL-rgt-lft} = & \lft(\rgt(b)) \\ & \let{x = \lft(\rgt(b))} = & x \end{eqnarray*}\] and if \(x = \rgt(c)\), note that \[\begin{eqnarray*} & & \compose(\uAssocL)(\uAssocR)(x) \\ & \let{x = \rgt(c)} = & \compose(\uAssocL)(\uAssocR)(\rgt(c)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \uAssocL(\uAssocR(\rgt(c))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uAssocR-rgt} = & \uAssocL(\rgt(\rgt(c))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-uAssocL-rgt-rgt} = & \rgt(c) \\ & \let{x = \rgt(c)} = & x \end{eqnarray*}\] as needed.

_test_uassocL_lft :: (Equal a, Equal b, Equal c)
  => a -> b -> c -> Test (a -> Bool)
_test_uassocL_lft _ y z =
  testName "uassocL(lft(a)) == lft(lft(a))" $
  \a ->
    let w = (lft y) `withTypeOf` (rgt z)
    in eq
      (uassocL ((lft a) `withTypeOf` (rgt w)))
      (lft (lft a))


_test_uassocL_rgt_lft :: (Equal a, Equal b, Equal c)
  => a -> b -> c -> Test (b -> Bool)
_test_uassocL_rgt_lft x _ z =
  testName "uassocL(rgt(lft(b))) == lft(rgt(b))" $
  \b -> eq
    (uassocL 
      ((rgt ((lft b) `withTypeOf` (rgt z)) `withTypeOf` (lft x))))
    (lft (rgt b))


_test_uassocL_rgt_rgt :: (Equal a, Equal b, Equal c)
  => a -> b -> c -> Test (c -> Bool)
_test_uassocL_rgt_rgt x y _ =
  testName "uassocL(rgt(rgt(c))) == rgt(c)" $
  \c -> eq
    (uassocL
      ((rgt ((rgt c) `withTypeOf` (lft y)) `withTypeOf` (lft x))))
    (rgt c)


_test_uassocR_lft_lft :: (Equal a, Equal b, Equal c)
  => a -> b -> c -> Test (a -> Bool)
_test_uassocR_lft_lft _ y z =
  testName "uassocR(lft(lft(a))) == lft(a)" $
  \a -> eq
    (uassocR
      ((lft ((lft a) `withTypeOf` (rgt y)) `withTypeOf` (rgt z))))
    (lft a)


_test_uassocR_lft_rgt :: (Equal a, Equal b, Equal c)
  => a -> b -> c -> Test (b -> Bool)
_test_uassocR_lft_rgt x _ z =
  testName "uassocR(lft(rgt(b))) == rgt(lft(b))" $
  \b -> eq
    (uassocR
      ((lft ((rgt b) `withTypeOf` (lft x)) `withTypeOf` (rgt z))))
    (rgt (lft b))


_test_uassocR_rgt :: (Equal a, Equal b, Equal c)
  => a -> b -> c -> Test (c -> Bool)
_test_uassocR_rgt x y _ =
  testName "uassocR(rgt(c)) == rgt(rgt(c))" $
  \c ->
    let w = (lft x) `withTypeOf` (rgt y)
    in eq
      (uassocR ((rgt c) `withTypeOf` (lft w)))
      (rgt (rgt c))


_test_uassocR_uassocL :: (Equal a, Equal b, Equal c)
  => a -> b -> c -> Test (Union a (Union b c) -> Bool)
_test_uassocR_uassocL _ _ _ =
  testName "uassocR . uassocL == id" $
  \x -> eq (uassocR (uassocL x)) x


_test_uassocL_uassocR :: (Equal a, Equal b, Equal c)
  => a -> b -> c -> Test (Union (Union a b) c -> Bool)
_test_uassocL_uassocR _ _ _ =
  testName "uassocL . uassocR == id" $
  \x -> eq (uassocL (uassocR x)) x

We also define some helper functions which detect whether an element of \(A + B\) is a \(\lft\) or a \(\rgt\).

Let \(A\) and \(B\) be sets. We define \(\isLft : A + B \rightarrow \bool\) by \[\isLft = \either(\const(\btrue),\const(\bfalse))\] and \(\isRgt : A + B \rightarrow \bool\) by \[\isRgt = \either(\const(\bfalse),\const(\btrue)).\]

In Haskell:

isLft :: Union a b -> Bool
isLft = either (const true) (const false)

isRgt :: Union a b -> Bool
isRgt = either (const false) (const true)

Now \(\isLft\) and \(\isRgt\) have some nice properties.

Let \(A\) and \(B\) be sets. Then we have the following for all \(a \in A\) and \(b \in B\).

\(\isLft(\lft(a)) = \btrue\).
\(\isLft(\rgt(b)) = \bfalse\).
\(\isRgt(\lft(a)) = \bfalse\).
\(\isRgt(\rgt(b)) = \btrue\).

We have \[\begin{eqnarray*} & & \isLft(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#dfn-isLft} = & \either(\const(\btrue),\const(\bfalse))(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \const(\btrue)(a) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \btrue \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \isLft(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#dfn-isLft} = & \either(\const(\btrue),\const(\bfalse))(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \const(\bfalse)(b) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \bfalse \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \isRgt(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#dfn-isRgt} = & \either(\const(\bfalse),\const(\btrue))(\lft(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \const(\bfalse)(a) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \bfalse \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \isRgt(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#dfn-isRgt} = & \either(\const(\bfalse),\const(\btrue))(\rgt(b)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \const(\btrue)(b) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \btrue \end{eqnarray*}\] as claimed.

_test_isLft_lft :: (Equal a, Equal b)
  => a -> b -> Test (a -> Bool)
_test_isLft_lft _ y =
  testName "isLft(lft(a)) == true" $
  \a -> eq (isLft ((lft a) `withTypeOf` (rgt y))) true


_test_isLft_rgt :: (Equal a, Equal b)
  => a -> b -> Test (b -> Bool)
_test_isLft_rgt x _ =
  testName "isLft(rgt(b)) == false" $
  \b -> eq (isLft ((rgt b) `withTypeOf` (lft x))) false


_test_isRgt_lft :: (Equal a, Equal b)
  => a -> b -> Test (a -> Bool)
_test_isRgt_lft _ y =
  testName "isRgt(lft(a)) == false" $
  \a -> eq (isRgt ((lft a) `withTypeOf` (rgt y))) false


_test_isRgt_rgt :: (Equal a, Equal b)
  => a -> b -> Test (b -> Bool)
_test_isRgt_rgt x _ =
  testName "isRgt(rgt(b)) == true" $
  \b -> eq (isRgt ((rgt b) `withTypeOf` (lft x))) true

Testing

Suite:

_test_disjoint_union
  :: ( 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_disjoint_union size cases a b c = do
  testLabel3 "Disjoint Union" a b c
  let args = testArgs size cases

  runTest args (_test_either_lft_rgt a b)

  runTest args (_test_uswap_lft a b)
  runTest args (_test_uswap_rgt a b)
  runTest args (_test_uswap_uswap a b)

  runTest args (_test_upair_lft a b)
  runTest args (_test_upair_rgt a b)
  runTest args (_test_upair_upair a b)

  runTest args (_test_uassocL_lft a b c)
  runTest args (_test_uassocL_rgt_lft a b c)
  runTest args (_test_uassocL_rgt_rgt a b c)
  runTest args (_test_uassocR_lft_lft a b c)
  runTest args (_test_uassocR_lft_rgt a b c)
  runTest args (_test_uassocR_rgt a b c)
  runTest args (_test_uassocR_uassocL a b c)
  runTest args (_test_uassocL_uassocR a b c)

  runTest args (_test_isLft_lft a b)
  runTest args (_test_isLft_rgt a b)
  runTest args (_test_isRgt_lft a b)
  runTest args (_test_isRgt_rgt a b)

Main:

main_disjoint_union :: IO ()
main_disjoint_union = do
  _test_disjoint_union 20 100 (true :: Bool) (true :: Bool) (true :: Bool)

  let a = lft true :: Union Bool Bool

  _test_functions 20 100 a a a a
  _test_flip      20 100 a a a a a a a
  _test_clone     20 100 a a
  _test_compose   20 100 a a a a a a a