Coproduct.idr

Coproducts

Coproducts give the choice of one out of two possible types, once given a value of a coproduct we need to pattern-match to find out what value is actually carried. Here we define the coproduct type with the familiar $(+)$ operator that symbolises the sum. Each inhabitant of the coproduct uses a left (<+) prefix operator (see section \ref{unicode-and-operators}) or a right (+>) prefix operator to distinguish what value is being carried.

Definition

Coproducts are given by two constructors, one for the left choice (<+) and one for the right choice (+>)

data (+) : Type -> Type -> Type where
  ||| Left choice
  (<+) : a -> a + b
  ||| Right choice
  (+>) : b -> a + b

Proposition

Given two maps $a\to c$ and $b\to c$ we can eliminate a coproduct $a+b$ into a value $c$. This is the eliminator for coproducts, or equivalently, the universal property of coproducts.

choice : (a -> c) -> (b -> c) -> a + b -> c
choice f g (<+ x) = f x
choice f g (+> x) = g x

Proposition

The diagonal operator eliminates a coproduct if both sides are the same type.

dia : a + a -> a
dia (<+ x) = x
dia (+> x) = x

Proposition

Coproducts form a bifunctor on types.

Bifunctor (+) where
  bimap f g (<+ x) = <+ (f x)
  bimap f g (+> x) = +> (g x)

Proposition

Void is the neutral for the coproduct.

public export
getRight : Void + a -> a
getRight (<+ x) = void x
getRight (+> x) = x
 
public export
getLeft : a + Void  -> a
getLeft (<+ x) = x
getLeft (+> x) = void x

export
distribF : Functor f => f a + f b -> f (a + b)
distribF (<+ x) = map (<+) x
distribF (+> x) = map (+>) x

public export
dchoice : {0 a, b : Type} -> {0 c : a + b -> Type} ->
          ((x : a) -> c (<+ x)) -> ((x : b) -> c (+> x)) ->
          (x : a + b) -> c x
dchoice f g (<+ x) = f x
dchoice f g (+> x) = g x