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:

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

## 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 → (A ∪ B)
a = (a ∪ b)

inj₂ : {A B : Set} → B → (A ∪ B)
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:

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