Functional algorithmics (2) — Type operators and (higher) kinds
You’ve learnt in part 1 what basic and function types are. The umbrella term for these is proper types and they’re denoted by ∗. The collection of proper types is infinite since the type operator → can be used unboundedly ad infinitum. Let’s refer to this collection as T. In this part we’ll look at “user defined” type operators.
Type operators can be thought of as a simply typed λ-calculus with only one basic type, namely ∗. We’ve met one type operator so far, →, which is built into the formalism. However it turns out that it’s very useful for us to be able to define our own type operators. Consider a set of elements of a type α. We can define a type operator S which can be characterised as ∗→∗ in the λ-calculus “one level up” operating on ∗. For example Sω is the proper type of sets of natural numbers.
We could now have a function called card (short for “cardinality”) of type Sω→ω returning the number of elements of a set of natural numbers. Sω→ω is of course a proper type (∗). Note however that we don’t need to know the type of the elements of a set in order to just count them. What we need then is a function (characterised as ∗→∗) which can take as its argument any set, regardless of the type of its elements. We thus have
card ≡ (λt:∗) (λs:St) ...where … stand for the expression calculating the cardinality of a set once the type of its elements is known. Note that the type of card is no longer a member of T since ∗ isn’t one of its basic types so it’s not a proper type. Such types are called generic.
We’ve seen a function, card, whose type is a type operator which needs to be applied to a proper type in order to yield another proper type, in this case a function type. Such type operators form a collection which we might denote by T→T (sometimes it’s denoted by [T,T]) since it’s a collection of type-valued mappings from T into T.
Another example of a simple type operator are lists which are similar to sets but ordered, i.e., we have a type operator, L, and Lα is the type of lists whose elements are of type α. We could now have a generic function which takes a list and creates a set containing the same elements. It’s generic because the type of the elements is unspecified. It can be characterised as ∗→∗ and it’s type is Lα→Sα (note that α is a free variable here, once it’s fixed the type of the function is characterised as ∗).
We can also go one level up and define a function, clone, which takes any iterable collection (such as a list, binary tree or heap) and creates a set containing its elements. However this function, while generic, isn’t a member of T→T since one of the arguments of its type is generic. Such types are called higher-kinded. A kind is either ∗ or an expression made up of other kinds using →. In other words, then, higher-kinded types are type-valued higher-order functions. In particular, ∗ or ∗→∗ are not higher-kinded, while ∗→(∗→∗)→∗, the kind of clone, is higher-kinded. It’s worthy of note that most object-oriented (OO) languages don’t admit higher-kinded types. One notable exception is C++ whose type system allows for templates to be parameters of templates.
In sum, the kind of basic and function types is ∗, the kind of (generic) collections such as sets, lists and trees is ∗→∗ and these kinds are commonplace in most OO languages such as C++, Java, C#, Swift, Go, etc. However these languages (with the exception of C++) don’t admit higher-kinded types.
In part 3 we’ll prepare the ground for the explanation of monads.