Polymorphic Datatypes

Code sharing also applies to datatype declarations. For instance, a commonly used polymorphic datatype list0 is declared as follows:

datatype list0 (a:t@ype) = | list0_nil (a) of () | list0_cons (a) of (a, list0 a) // end of [list0]

More precisely, list0 is a type constructor. Given a type T, we can form a type list0(T) for lists consisting of elements of the type T. For instance, list0(char) is for character lists, list0(int) for integer lists, list0(list0(int)) for lists whose elements are themselves integer lists, etc. To a great extent, the need for function templates or polymorphic functions largely stems from the availability of polymorphic datatypes. As an example, a function template list0_length is implemented as follows for computing the length of any given list:

fun{a:t@ype} list0_length (xs: list0 a): int = ( case+ xs of | list0_cons (_, xs) => 1 + list0_length<a> (xs) | list0_nil () => 0 ) (* end of [list0_length] *)

When applying list0_length to a list xs, we can in general write list0_length(xs), expecting the typechecker to synthesize a proper type parameter for list0_length. We may also write list0_length<T>(xs) if the elements of xs are of the type T. The latter style, though a bit more verbose, is likely to yield more informative messages in case type-errors occur.

Another commonly used polymorphic datatype option0 is declared as follows:

datatype option0 (a:t@ype) = | option0_none (a) of () | option0_some (a) of a // end of [option0]

A typical use of option0 is to perform some kind of error-handling. Suppose that we are to implement a function doing integer division and we want to make sure that the function returns even if it is called in a case where the divisor equals 0. This can be done as follows:

fun divopt ( x: int, y: int ) : option0 (int) = if y != 0 then option0_some{int}(x/y) else option0_none((*void*)) // end of [divopt]

By inspecting what divopt returns, we can tell whether integer division has been done normally or an error of divsion-by-zero has occurred. A realistic use of option0 is shown in the following implementation of list0_last:

fun{ a:t@ype } list0_last ( xs: list0 a ) : option0 (a) = let // fun loop (x: a, xs: list0 a): a = ( case+ xs of | list0_nil () => x | list0_cons (x, xs) => loop (x, xs) ) (* end of [loop] *) // in case+ xs of | list0_nil () => option0_none((*void*)) | list0_cons (x, xs) => option0_some{a}(loop (x, xs)) end // end of [list0_last]

When applied to a list, list0_last returns an optional value. If the value matches the pattern option0_none(), then the list is empty. Otherwise, the value is formed by applying option0_some to the last element of the given list.