# Structural types¶

In addition to the primitive types covered so far, disco also has sum and product types which can be used to build up more complex structures out of simpler ones.

## Product types¶

The product of two types, written using an asterisk `*`

or Unicode
times symbol `×`

, is a type whose values are ordered pairs of values
of the component types. Pairs are written using standard ordered pair
notation.

```
pair1 : N * Q
pair1 = (3, -5/6)
pair2 : Z5 × Bool
pair2 = (17 + 22, (3,5) < (4,2))
pair3 : Bool * (Bool * Bool)
pair3 = (true, (false, true))
pair4 : Bool * Bool * Bool
pair4 = (true, false, true)
```

`pair1`

in the example above has type `N * Q`

, that is, the type
of pairs of a natural number and a rational number; it is defined to
be the pair containing `3`

and `-5/6`

. `pair2`

has type ```
Z5 ×
Bool
```

(using the alternate syntax `×`

in place of `*`

), and
contains two values: \((17 + 22) \pmod{5}\), and the result of
asking whether \((3,5) < (4,2)\).

```
Disco> pair2
(4, true)
```

Pairs are compared lexicographically, which intuitively means that the
first component is most important, the second component breaks ties in
the first component, and so on. For example, \((a,b) < (c,d)\) if
either \(a < c\) (in which case \(b\) and \(d\) don’t
matter) or if \(a = c\) and \(b < d\). This is why ```
(3,5) <
(4,2)
```

evaluates to `true`

. Of course, two pairs are equal exactly
when their first elements are equal and their second elements are
equal.

`pair3`

shows that pairs can be nested: it is a pair whose second
component is also a pair. `pair4`

looks like an ordered triple, but
in fact we can check that `pair3`

and `pair4`

are equal!

```
Disco> pair3 = pair4
true
```

Really, `pair4`

is just syntax sugar for `pair3`

. In general:

- The type
`X * Y * Z`

is interpreted as`X * (Y * Z)`

. - The tuple
`(x,y,z)`

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

.

This continues recursively, so, for example, `A * B * C * D * E`

means `A * (B * (C * (D * E)))`

. Put another way, disco really only
has pairs, but appears to support arbitrarily large tuples by encoding
them as right-nested pairs.

If you want *left*-nested pairs you can use explicit parentheses: for
example, `(Bool * Bool) * Bool`

is not the same as ```
Bool * Bool *
Bool
```

, and has values such as `((false, true), true)`

.

## Sum types¶

If `X`

and `Y`

are types, their *sum*, written `X + Y`

(or ```
X ⊎
Y
```

), is the disjoint union of `X`

and `Y`

. That is, values of
type `X + Y`

are either values of `X`

or values of `Y`

, along
with a “tag” so that we know which it is. The possible tags are
`left`

and `right`

(to indicate the type on the left or right of
the `+`

). For example:

```
sum1 : N + Bool
sum1 = left 3
sum2 : N + Bool
sum2 = right false
sum3 : N + N + N
sum3 = right (right 3)
```

`sum1`

and `sum2`

have the same type, namely, `N + Bool`

; values
of this type consist of either a natural number or a boolean.
`sum1`

contains a natural number, tagged with `left`

; `sum2`

contains a boolean tagged with `right`

.

Notice that `X + X`

is a different type than `X`

, because we get
two distinct copies of all the values in `X`

, some tagged with
`left`

and some with `right`

. This is why we call a sum type a
*disjoint* union.

Iterated sum types, as in `sum3`

, are handled in exactly the same
way as iterated product types: `N + N + N`

is really syntax sugar
for `N + (N + N)`

. `sum3`

therefore begins with a `right`

tag,
to show that it contains a value of the right-hand type, namely, ```
N +
N
```

; this value in turn consists of another `right`

tag along with a
value of type `N`

. Other values of the same type `N + N + N`

include `right (left 6)`

and `left 5`

.

## Unit and Void types¶

Disco has two other special built-in types which are rarely useful on their own, but often play an important role in describing other types.

The type

`Unit`

has just a single value, called`()`

.Disco> :type () () : Unit

It is isomorphic to the type

`Z1`

.The type

`Void`

has*no*values. It is also isomorphic to`Z0`

.

## Counting and enumerating types¶

For any type which has only a finite number of values, disco can count
how many values there are, using the `count`

operator, or list them
using `enumerate`

(we will learn more about lists later in the
tutorial).

```
Disco> count ((Z2 * Z4) + Bool)
right 10
Disco> enumerate ((Z2 * Z4) + Bool)
[left (0, 0), left (0, 1), left (0, 2), left (0, 3),
left (1, 0), left (1, 1), left (1, 2), left (1, 3),
right false, right true]
Disco> enumerate (Bool * Bool * Bool)
[(false, false, false), (false, false, true), (false, true, false), (false, true, true),
(true, false, false), (true, false, true), (true, true, false), (true, true, true)]
```