Recursively Defined Datatypes

A recursively defined datatype (or recursive datatype for short) is one such that its associated constructors may form values by applying to values of the datatype itself. For instance, the following declared datatype charlst is recursive:

```datatype charlst =
| charlst_nil of ()
| charlst_cons of (char, charlst)
// end of [charlst]
```

When applied to a character and a value of the type charlst, the constructor charlst_cons forms a value of the type charlst. As an example, the following value represents a character list consisting of 'a', 'b' and 'c':

```charlst_cons('a', charlst_cons('b', charlst_cons('c', charlst_nil())))
```

We can define a function charlst_length as follows to compute the length of a given character list:

```fun
charlst_length
(
cs: charlst
) : int =
case cs of
| charlst_nil() => 0
| charlst_cons(_, cs) => 1 + charlst_length(cs)
// end of [charlst_length]
```

Note that this implementation is recursive but not tail-recursive. By relying on the commutativity and associativity of integer addition, we can give the following implementation of charlst_length that is tail-recursive:

```fun
charlst_length
(cs: charlst): int = let
//
fun loop
(cs: charlst, n: int): int = case cs of
| charlst_nil() => n | charlst_cons (_, cs) => loop(cs, n+1)
// end of [loop]
//
in
loop (cs, 0)
end // end of [charlst_length]
```

Note that the naming convention I follow closely in this book (and elsewhere) mandates that only a tail-recursive function be given a name indicative of its being a loop. A non-tail-recursive function is not called a loop because it cannot be translated directly to a loop in an imperative programming language like C.