understanding higher-kinded types

topics: ,

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!

List4 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 Maybe5. Together, these are first-order types.

Pair, HashMap6, and Either7 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.

more from the friends of danso:

I Can't Sleep

February 12

Me: "Seth Rogan?" Wife: "Yeah, what about him?" Me: "He's one of the good ones" Wife: "Ah! Good. I always liked him." It's been a mad couple of months in this house. It probably started on New Years Eve…

via Searching For Tao

Simple Precedence

February 4

A discussion between Jonathan Blow and Casey Muratori on the handling of precedence in Jon’s compiler recently popped in my YouTube feed. The discussion is three hours long and focuses on implementing operator precedence more easily and more simply in Jai…

via Reasonable Performance

Iron, man

December 31

Did you know that iron deficiency is the most common nutritional deficiency in the world? I did not. What’s weird about it is that while there are many symptoms, they can be misconstrued as signs stemming from other causes. Tired in the afternoon? Oh well…

via Hey Heather, it’s me again.

generated by openring