understanding higher-kinded types

posted on February 27, 12022 HE

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.¹ 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. ²

first-order types

There are also values of type List(Integer)³ such as [1,2,3] and [] , so List(Integer) has kind Type. But there are no values of type List!

List⁴ 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⁵. Together, these are first-order types.

Pair, HashMap⁶, and Either⁷ 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. ⁸

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 }. ⁹

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 that Integer 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 kind Type. 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 type String -> or -> Integer.

There are values of type String -> Integer, such as the length function where length(s) is the number of characters in s.

Expressing functions using the -> syntax can hide the fact that Function is really just a type of kind (Type,Type) -> Type like any other. You can think of String -> Integer as Function(String,Integer) if you prefer.↩︎
In functional programming languages, these kinds are often curried. Instead of (Type,Type) -> Type, HashMap might have kind Type -> (Type -> Type). A value would have type HashMap(String)(Integer).↩︎

more from the friends of danso:

ETS Match Specification Pitfall: Maps

February 9

During my work, I had a problem where I needed to efficiently write tree-shaped data. I also needed the ability to query ranges of the data. I reached for ETS tables, using the ordered_set table setting, and relied on match specifications to read ranges from the…

via Richard Kallos

Dan Savage on the Recent Inauguration

January 30

I've been reading and listening to Dan Savage for decades. He's a sex & advice columnist that started out in the back pages of a Seattle Weekly but who's grown in reach and popularity dramatically over the years. He spearheaded oppositio…

via Searching For Tao

Development of rustc_codegen_gcc #2

January 30

A couple months ago, I wrote an article that described the challenges we had to do the previous sync from the Rust repo to rustc_codegen_gcc. (if you don’t know what a sync is, please read that blog article). We also had many...

via Antoyo's Blog

generated by openring