Disjoint Unions

Posted on 2017-12-21 by nbloomf

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.

1. If $$x \in A + B$$, then either $$x = \lft(a)$$ for some $$a \in A$$ or $$x = \rgt(b)$$ for some $$b \in B$$.
2. 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$$.
3. $$\lft : A \rightarrow A+B$$ and $$\rgt : B \rightarrow A+B$$ are injective.
1. 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.
2. 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.
3. 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$$. 1. $$\uSwap(\lft(a)) = \rgt(a)$$. 2. $$\uSwap(\rgt(b)) = \lft(b)$$. 3. $$\compose(\uSwap)(\uSwap) = \id$$. 1. 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. 2. 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. 3. 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)).$

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.

1. $$\uPair(f,g)(\lft(a)) = \lft(f(a))$$.
2. $$\uPair(f,g)(\rgt(b)) = \rgt(g(b))$$.
3. $$\compose(\uPair(f,g))(\uPair(h,k)) = \uPair(\compose(f)(h),\compose(g)(k))$$.
1. 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.
2. 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.
3. 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. 1. $$\uAssocL(\lft(a)) = \lft(\lft(a))$$. 2. $$\uAssocL(\rgt(\lft(b))) = \lft(\rgt(b))$$. 3. $$\uAssocL(\rgt(\rgt(c))) = \rgt(c)$$. 4. $$\uAssocR(\lft(\lft(a))) = \lft(a)$$. 5. $$\uAssocR(\lft(\rgt(b))) = \rgt(\lft(b))$$. 6. $$\uAssocR(\rgt(c)) = \rgt(\rgt(c))$$. 7. $$\compose(\uAssocR)(\uAssocL) = \id_{A + (B + C)}$$. 8. $$\compose(\uAssocL)(\uAssocR) = \id_{(A + B) + C}$$. 1. 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. 2. 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. 3. 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. 4. 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. 5. 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. 6. 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. 7. 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. 8. 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$$. 1. $$\isLft(\lft(a)) = \btrue$$. 2. $$\isLft(\rgt(b)) = \bfalse$$. 3. $$\isRgt(\lft(a)) = \bfalse$$. 4. $$\isRgt(\rgt(b)) = \btrue$$. 1. 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. 2. 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. 3. 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. 4. 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