# 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 solely`type`

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
```