Types

Every value in disco has a type. Types play a central role in the language, and help guide and constrain programs. All the types in a program must match correctly (i.e. the program must typecheck) before it can be run. The type system has for the most part been designed to correspond to common mathematical practice, so if you are used to type systems in other programming languages (even other functional languages) you may be in for a surprise or two.

Disco can often infer the type of an expression. To find out what type disco has inferred for a given expression, you can use the :type command. For example:

Disco> :type 3
3 : ℕ
Disco> :type 2/3
2 / 3 : 𝔽
Disco> :type [1,2,5]
[1, 2, 5] : List ℕ

The colon in 3 : ℕ can be read “has type” or “is a”, as in “three is a natural number”. A colon can also be used to give an explicit type to an expression, for example, when you want to specify a type other than what disco would infer. For example:

Disco> :type 3 + 5
3 + 5 : ℕ
Disco> :type (3 : Integer) + 5
(3 : ℤ) + 5 : ℤ

The above example shows that normally, disco infers the type of 3 + 5 to be a natural number, but we can force the 3 to be treated as an Integer, which in turn forces the whole expression to be inferred as an integer.

Primitive numeric types

Disco has four built-in primitive numeric types: natural numbers, integers, fractions (i.e. nonnegative rationals), and rationals.

  • The type of natural numbers, written Natural, Nat, N, or ℕ, includes the counting numbers \(0, 1, 2, \dots\).
  • The type of integers, written Integer, Int, Z, or ℤ, includes the natural numbers as well as their negatives.
  • The type of fractions (i.e. nonnegative rationals), written Fractional, Frac, F, or 𝔽, includes all ratios of the form \(a/b\) where \(a\) and \(b\) are natural numbers, with \(b \neq 0\).
  • The type of rational numbers, written Rational, Q or ℚ, includes all ratios of integers.

In mathematics, it is typically not so common to think of the nonnegative rationals \(\mathbb{F}\) as a separate set by themselves; but this is mostly for historical reasons and because of the way the development of rational numbers is usually presented. The natural numbers support addition and multiplication. Extending them to support subtraction yields the integers; then, extending these again to support division yields the rationals. However, what if we do these extensions in the opposite order? Extending the natural numbers to support division results in the positive rational numbers; then extending these with subtraction again yields the rationals. All told, the relationship between these four types forms a diamond-shaped lattice:

  Q
 / \
Z   F
 \ /
  N

Each type is a subset of the type or types above it. Going northwest in this diagram (\(\mathbb{N} \to \mathbb{Z}\) or \(\mathbb{F} \to \mathbb{Q}\)) corresponds to allowing negatives, that is, subtraction; going northeast (\(\mathbb{N} \to \mathbb{F}\) or \(\mathbb{Z} \to \mathbb{Q}\)) corresponds to allowing reciprocals, that is, division.

Try evaluating each of the following expressions at the disco prompt, and also request their inferred type with the :type command. What type does disco infer for each? Why?

  • 1 + 2
  • 3 * 7
  • 1 - 2
  • 1 / 2
  • (1 - 2) / 3

Going southeast in the lattice (getting rid of negatives) is accomplished with the absolute value function abs. Going southwest (getting rid of fractions) is accomplished with floor and ceiling.

Note that disco supports subtyping, that is, values of type S can be automatically “upgraded” to another type T as long as S is a “subtype” (think: subset) of T. For example, a natural number can be automatically upgraded to an integer.

Disco> (-1 : Z) + (3 : N)
2
Disco> :type (-1 : Z) + (3: N)
(-1 : ℤ) + (3 : ℕ) : ℤ

In the above example, the natural number 3 is automatically upgraded to an integer so that it can be added to -1. When we discuss functions later, we will see that this principle extends to function arguments as well: for example, if a function is expecting an integer as input, it is acceptable to give it a natural number, since the natural number can be upgraded to an integer.

Other types

There are many other types built into disco as well—Bool, Void, Unit, List, product, and sum types, to name a few. These will be covered throughout the rest of the tutorial in appropriate places. For now, try executing these commands and see if you can guess what is going on:

  • :type false
  • :type unit
  • :type [1, 2, 3]
  • :type [1, 2, -3]
  • :type [1, 2, -3, 4/5]
  • :type [[1,2], [3,4,5]]
  • :type (1, true)
  • :type left(3)