Subtypes

In some cases, Disco is willing to accept one type in place of another, when this is known to be safe. For example, suppose we have the following definitions:

f : N -> N
f(n) = sqrt(n) + 1

g : Z -> Z
g(n) = n - 5

x : N
x = 16

y : Z
y = -10

Of course we can give x as an input to f, because the type of f says it takes natural numbers as input, and x is a natural number. Likewise, the type of y matches g’s input type, so we can give y as an input to g:

Disco> f(x)
5
Disco> g(y)
-15

On the other hand, we cannot give y as an input to f. f is expecting only natural numbers as input, and it might not be safe to give it a negative number. In fact, in this case, it’s definitely not safe: we cannot take the square root of a negative number.

Disco> f(y)
Error: typechecking failed.
https://disco-lang.readthedocs.io/en/latest/reference/typecheck-fail.html

However, we can give x as an input to g:

Disco> g(x)
11

Why is that? Well, mathematically speaking, every natural number is also an integer, so if a function is prepared to receive any integer (positive or negative) as input, then giving it only natural numbers (i.e. nonnegative integers) is perfectly safe. Intuitively, disco automatically “converts” the natural number into an integer before giving it to g.

Since it is always safe to use a natural number anywhere an integer is expected, we say that N is a subtype of Z.

The four basic numeric types can be arranged in a diamond shape, like so:

Diamond lattice

Each type is a subtype of the type or types above it. That is, Z is a subtype of Q, F is a subtype of Q, and N is a subtype of all the others.

Subtyping for algebraic types

In addition to the subtype relationships between the basic numeric types, more complex algebraic types can be subtypes of each other too.

  • For pair types, A * B is a subtype of C * D exactly when A is a subtype of C, and B is a subtype of D. For example, given these definitions:

    g : Z * Q -> Q
g(x,y) = y / (3x)

p : N * N
p = (2,5)

    It is allowed to give p as an input to g:

    Disco> p(g)
5/6

    Since N is a subtype of Z, and N is a subtype of Q, therefore N * N is a subtype of Z * Q.

  • Similarly, for sum types, A + B is a subtype of C + D exactly when A is a subtype of C, and B is a subtype of D. For example, given these definitions:

    g : Z + Q -> Q
g(left(z)) = z / 2
g(right(y)) = 3y

p : N + Z
p = left(1)

r : N + Z
r = right(-2)

    It is allowed to give p and r as inputs to g:

    Disco> g(p)
1/2
Disco> g(r)
-6

    Since N is a subtype of Z, and N is a subtype of Q, therefore N + N is a subtype of Z + Q.

  • Function types work a little differently. A -> B is a subtype of C -> D exactly when C is a subtype of A and B is a subtype of D. Notice how the relationship is reversed for the input types. Working out why this makes sense is left as an interesting exercise for the reader.