What is a "kind" in the context of Type Systems?
In short: a kind is to types what a type is to values.
What is a value? 1
, 2
, 3
are values. So are "Hello"
and "World"
, true
and false
, and so forth.
Values belong to types. Types describe a set of values. 1
, 2
and 3
belong to the type Nat
, "Hello"
and "World"
to the type Text
, true
and false
to the type Boolean
.
Functions take one or more values as arguments and produce one or more values as results. In order to meaningfully do something with the arguments, the function needs to make some assumptions about them, this is done by constraining their types. So, function parameters and return values typically also have types.
Now, a function also has a type, which is described by the types of its inputs and outputs. For example, the abs
function which computes the absolute value of a number has the type
Number -> NonNegativeNumber
The function add
which adds two numbers has the type
(Number, Number) -> Number
The function divmod
has the type
(Number, Number) -> (Number, Number)
Okay, but if functions take values as arguments and produce values as results, and functions are values, then functions can also take functions as arguments and return functions as results, right? What's the type of such a function?
Let's say we have a function findCrossing
which finds the point where some other function (of numbers) crosses the y-axis. It takes as an argument the function and produces as a result a number:
(Number -> Number) -> Number
Or a function makeAdder
which produces a function which takes a number and adds a specific number to it:
Number -> (Number -> Number)
And a function which computes the derivative of another function:
(Number -> Number) -> (Number -> Number)
Let's look at the level of abstraction here: a value is something very concrete. It only means one thing. If we were to order our levels of abstraction here, we could say that a value has the order 0.
A function, OTOH is more abstract: a single function can produce many different values. So, it has order 1.
A function which returns or accepts a function is even more abstract: it can produce many different functions which can produce many different values. It has order 2.
Generally, we call everything with an order > 1 "higher order".
Okay, but what about kinds? Well, we said above that 1
, 2
, "Hello"
, false
etc. have types. But what is the type of Number
? Or Text
? Or Boolean
?
Well, its type is Type
, of course! This "type of a type" is called a kind.
And just like we can have functions which construct values out of values, we can have functions which construct types out of types. These functions are called type constructors.
And just like functions have types, type constructors have kinds. For example, the List
type constructor, which takes an element type and produces a list type for that element has kind
Type -> Type
The Map
type constructor, which takes a key type and a value type and produces a map type has kind
(Type, Type) -> Type
Now, continuing the analogy, if we can have functions which take functions as arguments, can we also have type constructors which take type constructors as arguments? Of course!
An example is the Functor
type constructor. It takes a type constructor and produces a type:
(Type -> Type) -> Type
Notice how we always write Type
here? Above, we had many different types like Number
, Text
, Boolean
etc. Here, we always have only kind of type, namely Type
. That gets tedious to (warning, bad pun ahead) type, so instead of writing Type
everywhere, we just write *
. I.e. Functor
has the kind
(* -> *) -> *
and Number
has the kind
*
Continuing the analogy, Number
, Text
and all others of kind *
have order 0, List
and all others of kind * -> *
or more generally (*, …) -> (*, …)
have order 1, Functor
and all of kind (* -> *) -> *
or * -> (* -> *)
(and so forth) have order 2. Except in this case we sometimes also call it rank instead of order.
Everything above order/rank 1 is called higher-order, higher-rank or higher-kinded.
I hope the analogy is clear now: types describe sets of values; kinds describe sets of types.
Aside: I completely ignored currying. Basically, currying means that you can transform any function which takes two values into a function which takes one value and returns a function which takes the other value, similarly for three, four, five, … arguments. This means that you only ever need to deal with functions with exactly one parameter, which makes languages much simpler.
However, this also means that technically speaking, add
is a higher-order function (because it returns a function) which is muddying the definitions.
The most eloquent explanation for kinds/higher-kinds I've seen so far and also in the context of Scala is Daniel Spiewak's High Wizardry in the Land of Scala. There are many versions, he gave this talk a few times, here I've chosen the longest one, but you can quickly google and find others.
The most important message from this talk is exactly the answer given by @Jörg W Mittag:
"kind is to types what a type is to values"
Another place for a more theoretical view on the subject is the paper Generics of a Higher Kind, also in the context of Scala.