Templates and Kinds in ALFE

Programmers work with values like 4 and "hydroxylic". We also generally work with variables like count and acid. Each variable holds precisely one value. But in many languages, not every variable can hold any value. In a statically typed language, count might be able to hold 4 and acid might be able to hold "hydroxylic", but not the other way around. That quality of variables and values that determines which objects can fit into which boxes is called type. So count might have a type of Integer and acid might have a type of String. Then if you have a function called square which multiplies its argument by itself and returns the result, it makes sense to say square(count) but not to say square(acid) - the latter is an error which is detected and flagged as quickly as possible (when the program is compiled, if not when it's typed in in the first place). On this blog, as a notational convention, types (and more generally type constructors, see below) start with a capital letter and variables and values don't. I think this is a useful convention, and some languages (including the language I am writing) enforce it.

A type constructor is a generalization of a type. It's either a type itself (which can be used to declare variables) or a template type constructor, a "function" of sorts which, when given another type constructor, yields a third type constructor. C++, C# and Java programmers are familiar with these "functions" - they're called templates or generics. A good example of a template type constructor is Array. You give it a type like String and you get back Array<String> (i.e. an array of strings). You can also have Array<Array<String>> if you're feeling adventurous. A type constructor can have multiple arguments, so you might have Pair<Integer, String> which (through the magic of something called currying) is the same thing as Pair<Integer><String>.

What if you have a template type constructor with a parameter that is not a type but is itself a template type constructor? Well, you can do that too - say you have a type constructor called FooCollection and you pass it Array (note, not Array<Integer> or Array<String>, which are types, just plain Array) and you get back FooCollection<Array> which might be implemented in terms of Array<Foo>. Similarly, FooCollection<List> might be implemented in terms of List<Foo>.

So if the type of the argument of square is Integer, how do we talk about the argument of FooCollection. We can't say "the type of the argument of FooCollection" because what it accepts isn't a type - a type constructor can't have a type, type is a kind of type constructor. And in fact that is exactly the word we use instead: "the kind of the argument of FooCollection is <>." Other examples of kinds are (nothing, i.e. the empty string) which is the kind of types like Integer and String (no angle brackets follow them), <><> aka <,> (which is the kind of Pair - i.e. you need to give it two types to get back a type) and <<>> (which is the kind of FooCollection - i.e. you need to give it a type constructor of kind <> to get back a type). The wikipedia article on kinds uses a different notation further removed from the C++-inspired one I use here, but the two are equivalent and the transformation from one to the other is purely mechanical.

Incidentally, you can refer to kinds in C++ as well - instead of the empty string for the kind of types, C++ uses "class" (a rather confusing overload of the word - distinct from "a structured type with default accessibility private") or "typename" which is a bit better. Instead of <>, C++ uses "template<typename>", instead of <><>, C++ uses "template<typename, typename>" (C++ has no currying) and instead of <<>> C++ uses "template<template<typename>>" (a so-called "template template parameter" - one of the more obscure areas of C++).

So we've gone from values to types to kinds, what comes next in the sequence? ("Sort?" that already has another meaning in computer science though.) Suppose you had a function which accepts a kind and returns another kind. My angle brackets here have that effect - they take a list of kinds and return a kind which is the kind of a type constructor that accepts type constructors of the listed kinds and returns a type. What a confusing sentence! Fortunately nobody to my knowledge has found a non-trivial use for anything one level up from kind. I say "fortunately" not just because it's really confusing but because we've run out of notation! If you start with a lower case letter to signify a value argument and an upper case letter to signify a type constructor argument, how do you signify a kind argument? Also, if we'd need to use different brackets (I almost wrote "a different kind of brackets" which would further confuse things - writing about this stuff is hard!) to distinguish kind functions from value functions and type constructor functions, and all the ASCII brackets already have other meanings in my language.

Anyway, this is the sort of thing that you bump your head against when you write compilers for languages which support templates. Fortunately, if you're just writing normal applications in this language you'll probably never need to be concerned with it. Until you do. At which point just doing the most obvious thing should work fine without any fuss. I think it's fun to think about though.

Leave a Reply