Menu
I have already read the Wikipedia article and searched for obvious places but I'm stuck. Can someone simple tell me what exactly is a Kind ? What is it used for ?
Scala examples are most appreciated
380
In the area of mathematical logic and computer science known as type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator. A kind system is essentially a simply typed lambda calculus "one level up", endowed with a primitive type, denoted.
The function KIND(var) returns the kind of the variable var. For example, the code integer(kind=4) :: i4 k = kind(i4) returns the value k = 4. Intrinsic types have a predetermined kind value.
In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old ones. Basic types are considered to be built using nullary type constructors.
Higher-kinded types are useful when we want to create a container that can hold any type of items; we don't need a different type for each specific content type.
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.
114
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.
22
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
