Type Definitions¶
The type
keyword can be used to conveniently declare aliases for
types. For example, consider the following function which takes a
list of natural number triplets and returns the sum of all the
triplets in the list:
sumTripletList : List (N * N * N) -> N
sumTripletList [] = 0
sumTripletList ((n1, n2, n3) :: rest) = (n1 + n2 + n3 + (sumTripletList rest))
Disco> sumTripletList [(1,2,3), (4,5,6)]
21
Let’s write the following type definition:
type NatTriple = N * N * N
The type NatTriple
is defined as a 3-tuple containing three values
of type N
. Note that in Disco, all type names must begin with a
capital letter. Now we can rewrite our type declaration for
sumTripletList
as follows:
sumTripletList : List(NatTriple) -> N
Recursive type definitions¶
However, type
definitions are in fact much more powerful. Disco
has no special syntax for declaring algebraic data types as in
Haskell, but unlike Haskell, type
definitions in Disco can be
recursive. Thus, we can build recursive algebraic data types
directly. For example, we can define a type of binary trees with
values of type N
at nodes as follows:
type Tree = Unit + (N * Tree * Tree)
Here, we see that a Tree
can either be a leaf, or a a triplet
containing a natural number value of the root as the first element,
and the left and right subtrees of type Tree
as the second and
third elements, respectively.
Given this definition of Tree
, here is how we would write a
function which takes a Tree
and returns the sum of all its node
values.
sumTree : Tree -> N
sumTree (left _) = 0
sumTree (right (n, l, r)) = n + sumTree(l) + sumTree(r)
Parameterized type definitions¶
Type definitions can also be parameterized. For example, we can make
the Tree
type polymorphic:
import list
type Tree(a) = Unit + (a * Tree(a) * Tree(a))
treeFold : b * (a * b * b -> b) * Tree(a) -> b
treeFold (z, f, left(unit)) = z
treeFold (z, f, right (a, l, r)) = f(a, treeFold(z,f,l), treeFold(z,f,r))
sumTree : Tree(Nat) -> Nat
sumTree(t) = treeFold(0, \(a,l,r). a+l+r, t)
flattenTree : Tree(a) -> List(a)
flattenTree(t) = treeFold([], \(a,l,r). append(l, append([a], r)), t)
Disco> :load example/tydefs-poly.disco
Disco> leaf = left(unit)
Disco> t = right (1, right (3, leaf, leaf), right (5, leaf, leaf)) : Tree N
Disco> sumTree(t)
9
Disco> flattenTree(t)
[3, 1, 5]
Cyclic type definitions¶
There is only one restriction on recursive type
definitions,
namely, they are not allowed to be cyclic, i.e. unguardedly
recursive. A type
definition is cyclic if the following two
conditions hold:
- Repeated expansions of the
type
definition yield solelytype
definitions. - The same
type
definition is encountered twice during repeated expansion.
For example:
-- Foo is not allowed because it expands to itself.
type Foo = Foo
-- Bar is not allowed: it expands to Baz which expands to Bar.
type Bar = Baz
type Baz = Bar
-- Pair is OK (though rather useless) because it expands to a
-- top-level type former (product) which is not a type definition.
type Pair = Pair * Pair