Processing math: 0%

Disjoint Unions

Posted on 2017-12-21 by nbloomf
Tags: literate-haskell, arithmetic-made-difficult

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.

  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.

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:

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.

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 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.

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:

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:

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.

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