Maths - Sum Types

Sum Type

Has multiple constructors but only one way to use it.

But the eliminator is more complicated than say, the product type, because we don't know if A+B will be decomposed into type A or type B.

sum type

Notation

In type theory the sum of A and B is denoted A+B. In logic the product is 'or' often denoted \/ .

An element of A+B is denoted <a,b> where 'a' is an element of 'A' and 'b' is an element of 'B'.

Rules

On the page about propositional logic here we had the introduction and elimination rules for 'or' :

Types are defined by their formation, term introduction, term eliminator and computation rules:

Introduction
Constructor		 Elimination
Deconstructor
A
A\/B
(\/I1)
B
A\/B
(\/I2)
A\/B [A]
...
C		 [B]
...
C
C
(\/E)

So the introduction rules show,

However we can't go in the reverse direction, for instance, if we have a proof of A \/ B we can't get to a proof of A. A proof of A \/ B does give us some information that is if:

Then we have a proof of C.

When we translate from propositional logic to type theory we get the corresponding example of a constructors and deconstructor for a sum type (Taken from Idris prelude here):

Constructors Deconstructor 
data Either : (a, b : Type) -> Type where
  ||| One possibility of the sum
  ||| conventionally used to
  ||| represent errors
  Left : (l : a) -> Either a b
  ||| The other possibility,
  ||| conventionally used to
  ||| represent success
  Right : (r : b) -> Either a b
 
||| Simply-typed eliminator for Either
||| @ f the action to take on Left
||| @ g the action to take on Right
||| @ e the sum to analyze
either : (f : Lazy (a -> c)) ->
           (g : Lazy (b -> c)) ->
           (e : Either a b) -> c
either l r (Left x)  = (Force l) x
either l r (Right x) = (Force r) x

So, like with the introduction rules, the constructors are easy:

As with the elimination rule, the Deconstructor is more complicated.

If we have a function (a -> c) and a function (b -> c) then we can generate a function: Either a b -> c

Another way to think about the deconstructor is as a matching operation, posibly implemented by a 'case' construct.

Rather than use the 'either' function above, it might be easier to use a 'case' construct: 
case x:(Either A B) of
   a => c
   b => c

So we can reformulate term eliminator rule as a matching operation. The above formulation told us that we can produce an element of C but here we make it explicit that this happens by matching on whether the element of A+B is an A or a B:

term eliminator rule

assume: a implies c
and b implies c
Γright adjointp:A+B   Γ a:Aright adjointcA :C   Γ b:Bright adjointcB :C
Γright adjointmatch(p, a.cA b.cB):C

β-reduction and η-reduction

β-reduction

construction followed by deconstruction:

η-reduction

deconstruction followed by construction:

Implementation in Idris for Sum

We can't constuct terms as easily because its more difficult to infer the type. 
Idris> :let M = Either Integer String
Idris> M
Either Integer String : Type
Idris> the M (Left 4)
Left 4 : Either Integer String
Idris> :let m = the M (Left 4)
Idris> m
Left 4 : Either Integer String
'case' as deconstructor 
lookup_default : Nat -> List a -> a -> a
lookup_default i xs def = case list_lookup i xs of
                              Nothing => def
                              Just x => x

Sum Type

ref

I think the + in A+B is thought of as an infix operator , we could write it as a prefix +(A,B) which makes it clearer that it is a type that depends on other types.

The usual axioms of products don't necessarily hold exactly, however they may hold upto isomorphism (or upto beta equality), that is, both sides of the equation contain the same information.

Type Term notes
A+B ≠ B+A inl(a) =? inr(a)  
(A+B)+C ≠A+(B+C)    
A+0 ≠A   0 can't be constructed so we are left with A=A
 

Sum Type

formation rule

right adjointA:Type   right adjointB:Type
right adjointA+B : Type
term introduction rule
Γright adjointa:A   Γright adjointb:B
Γright adjointinl(a): A+B   Γright adjointinr(b): A+B

term eliminator rule

assume: a implies c
and b implies c
Γright adjointp:A+B   Γ a:Aright adjointcA :C   Γ b:Bright adjointcB :C
Γright adjointmatch(p, a.cA b.cB):C

computation rule

beta reduction

match(inl(a), x.cA y.cB) =>β cA[a/x]
match(inr(b), x.cA y.cB) =>β cB[b/x]
Local completeness rule  

Implemetations of Sum

Idris

 
we could define a sum type like this:


data Or : Type -> Type -> Type where
   OrIntroLeft : a -> A a b
   OrIntroRight : b -> A a b

also there is a built in type 'Either':

from : Idris-dev/libs/prelude/Prelude/Either.idr

 
||| A sum type
data Either : (a, b : Type) -> Type where
  ||| One possibility of the sum,
  ||| conventionally used to represent errors
  Left : (l : a) -> Either a b
  ||| The other possibility, conventionally
  ||| used to represent success
  Right : (r : b) -> Either a b

-- Usage hints for erasure analysis
%used Left l
%used Right r

--------------------------------------------------------------------------------
-- Syntactic tests
--------------------------------------------------------------------------------

||| True if the argument is Left, False otherwise
isLeft : Either a b -> Bool
isLeft (Left l)  = True
isLeft (Right r) = False

||| True if the argument is Right, False otherwise
isRight : Either a b -> Bool
isRight (Left l)  = False
isRight (Right r) = True

--------------------------------------------------------------------------------
-- Misc.
--------------------------------------------------------------------------------

||| Simply-typed eliminator for Either
||| @ f the action to take on Left
||| @ g the action to take on Right
||| @ e the sum to analyze
either : (f : Lazy (a -> c)) ->
         (g : Lazy (b -> c)) ->
		 (e : Either a b) -> c
either l r (Left x)  = (Force l) x
either l r (Right x) = (Force r) x

COQ

from : coq/theories/Init/Datatypes.v

 
(** [sum A B], written [A + B], is the
	              disjoint sum of [A] and [B] *)

#[universes(template)]
Inductive sum (A B:Type) : Type :=
  | inl : A -> sum A B
  | inr : B -> sum A B.

Notation "x + y" := (sum x y) : type_scope.

Arguments inl {A B} _ , [A] B _.
Arguments inr {A B} _ , A [B] _.

Next Steps

Other types are discussed on the following pages:

 

metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.
flag flag flag flag flag flag Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.

 

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.