The basic syntax for a type definition is
type <Name> = <type>
<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
may then use
Count anywhere we want in place of
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
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
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
chain0) or another
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))