Type definitions

Disco has many built-in types, such as N, Bool, and so on. We can also define our own types, using the built-in types as building blocks.

Type synonyms

The basic syntax for a type definition is

type <Name> = <type>

The <Name> can be whatever name you want, but it must start with a capital letter. <type> can be any type expression.

One simple way use this is to define synonyms for existing types. For example:

type Count = N

f : Bool -> Count
f(True) = 1
f(False) = 0

In the above example, we define Count as a synonym for N; we may then use Count anywhere we want in place of N. Perhaps certain numbers represent some kind of count and we want to help ourselves document and remember what these numbers mean.

Somewhat more interestingly, we may define new names as abbreviations for more complex types. For example:

type Two = N*N
type OneOrTwo = N + Two

ensureTwo : OneOrTwo -> Two
ensureTwo(left(n)) = (n,n)
ensureTwo(right(p)) = p

Here we define OneOrTwo as a synonym for the type N + Two (which in turn means N + N*N), representing either a single natural number or a pair of natural numbers.

Recursive type definitions

Defining type names as synonyms for other types is convenient, but does not fundamentally add anything to the language. However, type definitions can also be recursive, that is, types can be defined in terms of themselves. This, it turns out, does give us a fundamentally new ability.

As a simple first example, consider the definition of the type Chain below:

type Chain = Unit + Chain

chain0 : Chain
chain0 = left(unit)

chain1 : Chain
chain1 = right(left(unit))

chain2 : Chain
chain2 = right(right(left(unit)))

Values of type Chain are defined as being either a Unit value (wrapped in left, like chain0) or another Chain value (wrapped in right, like chain1 or chain2). To make a Chain value, we can therefore keep choosing right as long as we want, until we finally stop with left(unit). So values of type Chain are actually very similar to natural numbers.

As another example, we could define binary trees of rational numbers like this:

type Tree = Unit + (Tree * Q * Tree)

leaf : Tree
leaf = left(unit)

tree1 : Tree
tree1 = right(leaf, 1/2, leaf)

tree2 : Tree
tree2 = right(tree1, 5/7, leaf)

Parameterized type definitions

It is also possible to create type definitions which have one or more type parameters. Type parameters are always written in parentheses. For example,

type Maybe(a) = Unit + a

type Tree(a) = Unit + (Tree(a) * a * Tree(a))

type FringyTree(a,b) = b + (FringyTree(a,b) * a * FringyTree(a,b))

When using a parameterized type, you can put whatever type you want in place of the parameters. For example,

x : Maybe(N)
x = right(3)

t : FringyTree(Bool, Q)
t = right(left(True), 2/3, left(False))