Product.idr

Products

The product of two types, pairs up two values and provides projections for each value. We use the traditional $(\ast )$ symbol to denote the product in Idris and π1 and π2 for its first and second projection. Its constructor is the (&&) operator borrowed from boolean conjunction, so that a && b reads “a and b”

Definition

Products in Idris are given by two types and projections ${\pi }_1$ and ${\pi }_2$.

record (*) (a, b : Type) where
  constructor (&&)
  π1 : a
  π2 : b

We also provide a number of helper functions for products but only showcase a selection of them here. The rest of them are in the appendix.

Proposition

Products form a Bifunctor.

Bifunctor (*) where
  bimap f g x = f x.π1 && g x.π2

Proposition

Functions can be curried.

curry : (a * b -> c) -> a -> b -> c
curry f a b = f (a && b)

Proposition

Functions can be uncurried.

uncurry : (a -> b -> c) -> a * b -> c
uncurry f x = f x.π1 x.π2

Proposition

Products associate from the left.

public export
assocL : (a * b) * c -> a * (b * c)
assocL x = x.π1.π1 && (x.π1.π2 && x.π2)

Proposition

Products associate from the right.

public export
assocR : a * (b * c) -> (a * b) * c
assocR x = (x.π1 && x.π2.π1) && x.π2.π2

Lemma

Pairing and projecting the first element gives back the first element

public export
proj1Pair : (0 a, b : _) -> (a && b).π1 === a
proj1Pair _ _ = Refl

Lemma

Pairing and projecting the second element gives back the second element

public export
proj2Pair : (0 a, b : _) -> (a && b).π2 === b
proj2Pair _ _ = Refl

Lemma

Projecting and pairing is the same as doing nothing

public export
projIdentity : (x : a * b) -> (x.π1 && x.π2) === x
projIdentity (a && b) = Refl