Contents Previous Next


module Types.product where

open import Lang.dataStructures using (
  Bool; true; false;
;; singleton;; List;
  one; two; three; four; five; six; seven; eight; nine; ten; zero; succ;
  _::_; [])

open import Agda.Primitive using (Level; __; lsuc; lzero)

Product types

A cartesian product of two types A and B can be defined as a pair of objects (a, b), where aA, and bB.

data _××_ (A B : Set) : Set where
  _,,_  : A  B  A ×× B

infixr 4 _××_

and cartesian products constructed as

oneTwo = one ,, two

oneTwoThree = one ,, (two ,, three)

Construction

While being intuitively familiar with what a cartesian product is, it’s algebraic definition captures the most abstract aspect of a product:

A cartesian product, in set theory, for two sets A and B is defined as:

A x B = { (a , b) | a ∈ A and b ∈ B }

In type theory, we look at another way of defining product types, just by looking at them as objects in themselves: For an object X, we call X a product type if:

  1. There exists two functions, lets call them proj₁ and proj₂ such that they can be used to “extract” the contents of the product X:
proj₁ : {A B : Set}  (A × B)  A
(a × b) = a

proj₂ : {A B : Set}  (A × B)  B
(a × b) = b
  1. If there is any another object A, such that the functions proj₁ₐ and proj₂ₐ satisfied the above condition for A, then there exists a function, fₐ₀ such that:
fₐ₀ : A  X

Note: The above is pseudo-code, the proof is below.

The second condition is the unique-ness condition, .i.e. for all objects having projections to A and B, there is one through which all projections go through. We call this one object the “Product” This is better visualized in this diagram:

Figure 1: Product

Dependent Pair Types or Σ-types

Dependent types are products where the 2nd type is dependent on the first one. They are of the form (x : A, B(x)). The notation in type theory looks like this for binary dependent pairs:

\[ \sum_{x : A} B(x) \]

with ternary dependent pair types being represented as:

\[ \sum_{x : A} \sum_{y : B(x)} C(y) \]

and so on.

Agda’s record types provides encapsulation for this definition and some syntactic sugars like constructors:

record Σ {a b} (A : Set a) (B : A  Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

infixr 4 _,_

While constructing complex mathematical structures, a fairly general pattern is that a bunch of properties can be bundled together to form objects, and then structures are built on top of them. Since all of those properties are types, a record containing a bunch of properties would by construction ensure the objects of such a record belong to the type represented. A lot of implementation of mathematical structures can be done in this form of records of bundled properties.

Hence if, say Prop₁ and Prop₂ are two properties, an object that satisfies both is a record with both properties as fields:

data prop1 : Set where
data prop2 : Set where

record Satisfies (x : prop1)(y : prop2) : Set where
  field
    p1 : prop1
    p2 : prop2

The record type is a special syntax for representing dependent or Σ (sigma) types in Agda, though they can very well also be represented in other ways such as using the data keyword.

Figure 2: Product (math)

API

Cross product

_×_ :  {a b} (A : Set a) (B : Set b)  Set (a ⊔ b)
A × B = Σ A  x  B)

Application of a product

<_,_> :  {a b c} {A : Set a} {B : A  Set b} {C :  {x}  B x  Set c}
        (f : (x : A)  B x)
         ((x : A)  C (f x))
         ((x : A)  Σ (B x) C)
< f , g > x = (f x , g x)

Map

Mapping a pair of functions f and g over a product:

map :  {a b p q} {A : Set a} {B : Set b} {P : A  Set p} {Q : B  Set q}
         (f : A  B)
         (∀ {x}  P x  Q (f x))
         Σ A P
         Σ B Q
map f g (x , y) = (f x , g y)

Swap

swap :  {a b} {A : Set a} {B : Set b}  A × B  B × A
swap (x , y) = (y , x)

Co-product types

Co-products, also called as “sum” types can be thought of as a disjoint uinon of two objects.

Mathematically, an object X ⋃ Y is a co-product of objects X and Y if,

  1. There exists two functions inj_₁ and inj₂ such that:
inj₁ : {A B : Set}  A  (AB)
a = (a ∪ b)

inj₂ : {A B : Set}  B  (AB)
b = (a ∪ b)
  1. If there is any another object A, such that the functions inj₁ₐ and inj₂ₐ satisfied the above condition, then there exists a function, fₐ₀ such that:
fₐ₀ : X  A
data __ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : (x : A)  A ∪ B
  inj₂ : (y : B)  A ∪ B

Co-product types are similar to product types, except with reversed arrows:

Figure 3: Coproducts

Maybe

Just like the cartesian product is the representative type of a product, the Maybe type fills that role for the co-product. This happens to be a very popular datatype in functional programming languages like haskell Maybe, scala Option etc and is widely used to error handling.

data Maybe {a} (A : Set a) : Set a where
  just    : (x : A)  Maybe A
  nothing : Maybe A

API

Eliminator

maybe :  {a b} {A : Set a} {B : Maybe A  Set b}
         ((x : A)  B (just x))
         B nothing
         (x : Maybe A)
         B x
maybe j n (just x) = j x
maybe j n nothing  = n

Map

A Maybe is also a structure which can be map-ed over:

smap :  {a b} {A : Set a} {B : Set b}  (A  B)  Maybe A  Maybe B
smap f (just x) = just (f x)
smap f nothing  = nothing

Zip

zip :  {a b c} {A : Set a} {B : Set b} {C : Set c}
         Maybe A
         Maybe B
         Maybe (A × B)
zip (just a) (just b) = just (a , b)
zip _ _ = nothing

Dependent Function Types / Π-types