# Pair types¶

*Pair types*, or *product types*, represent *ordered pairs* of
values. Suppose `A`

and `B`

are types. Then:

`A * B`

(also written`A × B`

) is a*pair type*(also known as a*product type*or*Cartesian product*). It represents the set of all possible pairs where the first element has type`A`

and the second element has type`B`

.A pair is written

`(a, b)`

(where`a`

and`b`

can be arbitrary expressions). Specifically, if`a : A`

and`b : B`

, then the ordered pair`(a, b)`

has type`A * B`

. For example:Disco> :type (1, True) (1, true) : ℕ × Bool Disco> :type (-7, -3) (-7, -3) : ℤ × ℤ

Pair types are commonly used to represent functions that take multiple
inputs. For example, `f : N * Z -> Q`

means that `f`

takes a
*pair* of a natural number and an integer as input. Such functions
are often defined via pattern matching on the pair,
like so:

```
f : N * Z -> Z
f(n,z) = 3n - z
```

## n-tuples and nested pairs¶

We have seen that `A * B`

is a type of *pairs* of values. What
about triples, quadruples, … n-tuples of values? The answer is
simple:

- triples are written
`(x,y,z)`

and have types like`A * B * C`

; - quadruples are written
`(w,x,y,z)`

and have types like`A * B * C * D`

; - and so on.

So, for example, a function taking a quintuple of values could be written like this:

```
funTaking5Tuple : N * Z * List(N) * Q * Bool -> Int
funTaking5Tuple(n,z,l,q,b) = ...
```

Note

General n-tuples actually are not specially built in at all:
rather, everything is actually built out of *nested pairs*. For
convenience, pair types and values both *associate to the right*,
that is,

- the type
`A * B * C`

is interpreted as`A * (B * C)`

, and - correspondingly,
`(x, y, z)`

is interpreted as`(x, (y, z))`

.

So, for example, the definition of the function `funTaking5Tuple`

from above is really shorthand for

```
funTaking5Tuple : N * (Z * (List(N) * (Q * Bool))) -> Int
funTaking5Tuple(n,(z,(l,(q,b)))) = ...
```

Typically one can just use triples or 5-tuples or whatever and not think about this, but occasionally it’s helpful to understand the way things are represented with nested pairs under the hood.