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.
The product of two types, written using an asterisk
* or Unicode
U+00d7 MULTIPLICATION SIGN), 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 : Z × 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
pair2 has type
Bool (using the alternate syntax
× in place of
contains two values: \(17 + 22\), and the result of
asking whether \((3,5) < (4,2)\).
Disco> pair2 (39, 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
(4,2) evaluates to
true. Of course, two pairs are equal exactly
when their first elements are equal and their second elements are
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
pair4 are equal!
Disco> pair3 == pair4 true
pair4 is just syntax sugar for
pair3. In general:
- The type
X * Y * Zis interpreted as
X * (Y * Z).
- The tuple
(x,y,z)is interpreted as
This continues recursively, so, for example,
A * B * C * D * E
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
(Bool * Bool) * Bool is not the same as
Bool * Bool *
Bool, and has values such as
((false, true), true).
Y are types, their sum, written
X + Y (or
U+228e MULTISET UNION), is the disjoint union of
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
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))
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
contains a boolean tagged with
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
Iterated sum types, as in
sum3, are handled in exactly the same
way as iterated product types:
N + N + N is really syntax sugar
N + (N + N).
sum3 therefore begins with a
to show that it contains a value of the right-hand type, namely,
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
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.
Unithas just a single value, called
Disco> :type unit ■ : Unit
Voidhas no values.
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
enumerate (we will learn more about lists later in the
Disco> count ((Bool * (Bool + Bool)) + Bool) right 10 Disco> enumerate ((Bool * (Bool + Bool)) + Bool) [left (false, left false), left (false, left true), left (false, right false), left (false, right true), left (true, left false), left (true, left true), left (true, right false), left (true, right true), 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)]