understanding higher-kinded types
Kinds are the types of types.
Okay, let me take a step back:
proper types
Values have types.
Some typical types are Integer
, Bool
, and String
.
Values of type Integer
include 0
, 1
, 42
.
Just as values can be grouped into types, types can be grouped into kinds.
Bool
and Integer
are among the simplest types.
We say that these types have kind Type
.1
Type
is the kind containing all populated types —
those types which have values.
Types of kind Type
are the only types
which can be thought of as sets of values,
like {true, false}
or {..., -2, -1, 0, 1, 2, ...}
.
Populated types are also called proper types.
2
first-order types
There are also values of type List(Integer)
3
such as [1,2,3]
and []
,
so List(Integer)
has kind Type
.
But there are no values of type List
!
List
4 is not a proper type.
In a certain sense, it needs another (proper) type to complete it.
We can think of List
as a function
whose domain and codomain are both proper types.
List
has kind Type -> Type
.
Other examples of types with kind Type -> Type
are Set
and Maybe
5.
Together, these are first-order types.
Pair
, HashMap
6, and Either
7
are not proper types either —
they are functions
whose domains are pairs of types
and whose codomains are types.
In other words, they have kind (Type,Type) -> Type
.
8
There are no values of type HashMap
,
nor any of type HashMap(String)
,
but there are values of type HashMap(String,Integer)
such as { "hello": 2 , "hi": 3 }
.
9
Types which require any number of other proper types as arguments to form proper types themselves are first-order types. First-order types effectively allow us to abstract over proper types.
beyond first-order
But first-order types do not allow us to abstract
over other first-order types.
There is no such thing as a List(List)
.
Believe it or not, there are some (useful!) types
which require first-order types to complete them.
These types have kinds such as (Type -> Type) -> Type
and are called higher-order or higher-kinded types.
Examples include Foldable, Traversable, Functor, and Monad.
Kinds and first-order types can help us understand type-classes (or generics) as a logical extension of the type system.
Higher-kinded types take that a step further and include first-order types in our generics. They provide the means to abstract over types which themselves abstract over types.
With thanks to hboo for revising an earlier draft of this post.
If you find it confusing that
Type
is the name of the kind containing all the types, remember thatInteger
is the name of the type containing all the integers!↩︎There’s a minor technical difference between a proper type and a populated type. A populated type has kind
Type
and there is at least one value of that type. A proper type meets the first requirement, but not necessarily the second.Void
is a type with no values (an empty set), but it still has kindType
. It is a proper type that is not populated.↩︎spelled with angle brackets in many languages, as in
List<Integer>
↩︎or
Array
↩︎or
Optional
↩︎or
Dict
↩︎or
Result
↩︎Also in this gang is
->
(function) — it has kind(Type,Type) -> Type
because it requires two types to complete it. In other words, there are no values of type->
, nor are there values of typeString ->
or-> Integer
.There are values of type
String -> Integer
, such as thelength
function wherelength(s)
is the number of characters ins
.Expressing functions using the
->
syntax can hide the fact thatFunction
is really just a type of kind(Type,Type) -> Type
like any other. You can think ofString -> Integer
asFunction(String,Integer)
if you prefer.↩︎In functional programming languages, these kinds are often curried. Instead of
(Type,Type) -> Type
,HashMap
might have kindType -> (Type -> Type)
. A value would have typeHashMap(String)(Integer)
.↩︎
more from the friends of danso:
rustc_codegen_gcc: Progress Report #21
March 13What is rustc_codegen_gcc? rustc_codegen_gcc is a GCC ahead-of-time codegen for rustc, meaning that it can be loaded by the existing rustc frontend, but benefits from GCC by having more architectures supported and having access to GCC’s optimizations. …
via Antoyo's BlogThe Tyranny of Existing Code
March 12Most programmers have experienced that feeling of worthlessness and powerlessness when we are trying to implement what should be a simple change, but the existing code base resists our attempts. Worse, often we can see what is causing us to be blocked, yet…
via Reasonable PerformanceThe Sustainable Travel Zone
January 5There's some exciting stuff happening here in Cambridge. The county council (the tier of government between municipal and national that handles Cambridge and the surrounding smaller towns) has declared that they want to build what they're calling…
via Searching For Taogenerated by openring