What's the difference between a type and a kind?

Question

I am learning the programming langauge Haskell, and I'm trying to wrap my head around what the difference between a type and a kind is.

As I understand it, a kind is a type of type. For instance, a ford is a type of car and a car is a kind of vehicle.

Is this a good way to think about this?

Because, the way my brain is currently wired, a ford is a **type** of car, but also a car is a **type** of vehicle whilst at the same time a car is a **kind** of vehicle. I.e. the terms type and kind are interchangeable.

Could anyone shed some light on this?

Answer 1

Here, "values", "types", and "kinds" have formal meanings, so considering their common English usage or analogies to classifying automobiles will only get you so far.

My answer pertains to the formal meanings of these terms in the context of Haskell specifically; these meanings are based on (though are not really identical to) the meanings used in mathematical/CS "type theory". So, this won't be a very good "computer science" answer, but it should serve as a pretty good Haskell answer.

In Haskell (and other languages), it ends up being helpful to assign a type to a program expression that describes the class of values the expression is permitted to have. I assume here that you've seen enough examples to understand why it would be useful to know that in the expression sqrt (a**2 + b**2), the variables a and b will always be values of type Double and not, say, String and Bool respectively. Basically, having types assists us in writing expressions/programs that will work correctly over a wide range of values.

Now, something you may not have realized is that Haskell types, like those that appear in type signatures:

fmap :: Functor f => (a -> b) -> f a -> f b

are actually themselves written in a type-level Haskell sublanguage. The program text Functor f => (a -> b) -> f a -> f b is -- quite literally -- a type expression written in this sublanguage. The sublanguage includes operators (e.g., -> is a right associative infix operator in this language), variables (e.g., f, a, and b), and "application" of one type expression to another (e.g., f a is f applied to a).

Did I mention how it was helpful in many languages to assign types to program expressions to describe classes of expression values? Well, in this type-level sublanguage, expressions evaluate to types (rather than values) and it ends up being helpful to assign kinds to type expressions to describe the classes of types they are permitted to represent. Basically, having kinds assists us in writing type expressions that will work correctly over a wide range of types.

So, values are to types as types are to kinds, and types help us write value-level programs while kinds help us write type-level programs.

What do these kinds look like? Well, consider the type signature:

id :: a -> a

If the type expression a -> a is to be valid, what kind of types should we permit variable a to be? Well, the type expressions:

Int -> Int
Bool -> Bool

look valid, so the types Int and Bool are obviously of the right kind. But even more complicated types like:

[Double] -> [Double]
Maybe [(Double,Int)] -> Maybe [(Double,Int)]

look valid. In fact, since we ought to be able to call id on functions, even:

(a -> a) -> (a -> a)

looks fine. So, Int, Bool, [Double], Maybe [(Double,Int)], and a -> a all look like types of the right kind.

In other words, it looks like there's only one kind, let's call it * like a Unix wildcard, and every type has the same kind *, end of story.

Right?

Well, not quite. It turns out that Maybe, all by itself, is just as valid a type expression as Maybe Int (in much the same way sqrt, all by itself, is just as valid a value expression as sqrt 25). However, the following type expression is not valid:

Maybe -> Maybe

Because, while Maybe is a type expression, it doesn't represent the kind of type that can have values. So, that's how we should define * -- it's the kind of types that have values; it includes "complete" types like Double or Maybe [(Double,Int)] but excludes incomplete, valueless types like Either String. For simplicity, I'll call these complete types of kind * "concrete types", though this terminology isn't universal, and "concrete types" might mean something very different to, say, a C++ programmer.

Now, in the type expression a -> a, as long as type a has kind * (the kind of concrete types), the result of the type expression a -> a will also have kind * (i.e., the kind of concrete types).

So, what kind of type is Maybe? Well, Maybe can be applied to a concrete type to yield another concrete type. So, Maybe looks like a little like a type-level function that takes a type of kind * and returns a type of kind *. If we had a value level function that took a value of type Int and returned a value of type Int, we'd give it a type signature Int -> Int, so by analogy we should give Maybe a kind signature * -> *. GHCi agrees:

> :kind Maybe
Maybe :: * -> *

Going back to:

fmap :: Functor f => (a -> b) -> f a -> f b

In this type signature, variable f has kind * -> * and variables a and b have kind *; the built-in operator -> has kind * -> * -> * (it takes a type of kind * on the left and one on the right and returns a type also of kind *). From this and the rules of kind inference, you can deduce that a -> b is a valid type with kind *, f a and f b are also valid types with kind *, and (a -> b) -> f a -> f b is valid type of kind *.

In other words, the compiler can "kind check" the type expression (a -> b) -> f a -> f b to verify it's valid for type variables of the right kind the same way it "type checks" sqrt (a**2 + b**2) to verify it's valid for variables of the right type.

The reason for using separate terms for "types" versus "kinds" (i.e., not talking about the "types of types") is mostly just to avoid confusion. The kinds above look very different from types and, at least at first, seem to behave quite differently. (For example, it takes some time to wrap your head around the idea that every "normal" type has the same kind * and the kind of a -> b is * not * -> *.)

Some of this is also historical. As GHC Haskell has evolved, the distinctions between values, types, and kinds have started to blur. These days, values can be "promoted" into types, and types and kinds are really the same thing. So, in modern Haskell, values both have types and ARE types (almost), and the kinds of types are just more types.

@user21820 asked for some additional explanation of "types and kinds are really the same thing". To be a little clearer, in modern GHC Haskell (since version 8.0.1, I think), types and kinds are treated uniformly in most of the compiler code. The compiler makes some effort in error messages to distinguish between "types" and "kinds", depending on whether it's complaining about the type of a value or the type of a type, respectively.

Also, if no extensions are enabled, they are easily distinguishable in the surface language. For example, types (of values) have a representation in the syntax (e.g., in type signatures), but kinds (of types) are -- I think -- completely implicit, and there's no explicit syntax where they appear.

But, if you turn on the appropriate extensions, the distinction between types and kinds largely disappears. For example:

{-# LANGUAGE GADTs, TypeInType #-}
data Foo where
  Bar :: Bool -> * -> Foo

Here, Bar is (both a value and) a type. As a type, its kind is Bool -> * -> Foo, which is a type-level function that takes a type of kind Bool (which is a type, but also a kind) and a type of kind * and produces a type of kind Foo. So:

type MyBar = Bar True Int

correctly kind-checks.

As @AndrejBauer explains in his answer, this failure to distinguish between types and kinds is unsafe -- having a type/kind * whose type/kind is itself (which is the case in modern Haskell) leads to paradoxes. However, Haskell's type system is already full of paradoxes because of non-termination, so it's not considered a big deal.

Answer 2

If you know about the difference between sets and classes in set theory, then it may help to think about the matter as $$\mathrm{type} : \mathrm{kind} = \mathrm{set} : \mathrm{class}.$$ If not, you can think of kinds as "large" or "higher" types whose elements may be types, or may involve types in some fashion. For example:

• Bool is a type
• Type is a kind because its elements are types
• Bool -> Int is a type
• Bool -> Type is a kind because its elements are functions that return types
• Bool * Int is a type
• Bool * Type is a kind because its elements are pairs with one component a type

In type theory it is usually undesirable to have the type of all types (it leads to pardoxes). Instead, we can have universes, which are types that contain other, smaller types. For instance, we might have a series of universes $U_0$, $U_1$, $U_2$, ... where $U_0$ contains basic stuff like $\mathtt{Bool}$, $\mathtt{Nat}$, $\mathtt{Nat} \to \mathtt{Nat}$, while $U_1$ contains $U_0$ and $\mathtt{Bool} \to U_0$ and $U_0 \to U_0$ etc. In general, $U_{n+1}$ contains $U_n$ as an element, as well as anything else we can build from $U_n$ and all the things that came before it, using the basic operations $\times$, $\to$, etc.

I am explaining all of this because often one only needs $U_0$ and $U_1$, in which case the elements of $U_0$ are usually called types and the elements of $U_1$ are called kinds. In Haskell terminology, the smallest univese $U_0$ is written as *. Thus * is an element of U_1, which Haskell does not name explicitly.

Answer 3

A value is like the specific red 2011 Ford Mustang with 19,206 miles on it that you have sitting in your driveway.

That specific value, informally, could have many types: it is a Mustang, and it is a Ford, and it is a car, and it is a vehicle, among many many other types that you could make up (the type of "things belonging to you", or the type of "things that are red", or...).

(In Haskell, to a first order approximation (GADTs break this property, and the magic around number literals and the OverloadedStrings extension obscure it a little), values have one principal type instead of the plethora of informal "types" you can give your 'stang. 42 is, for purposes of this explanation, an Int; there is no type in Haskell for "numbers" or "even integers"—or rather, you could make one, but it would be a disjoint type from Int.)

Now, "Mustang" may be a subtype of "car"—every value that is a Mustang is also a car. But the type—or, to use Haskell's terminology, the kind of "Mustang" is not "car". "Mustang" the type is not a thing you can park in your driveway or drive around in. "Mustang" is a noun, or a category, or just a type. Those are, informally, the kinds of "Mustang".

(Again, Haskell only recognises one kind for each type-level thing. So Int has kind *, and no other kinds. Maybe has kind * -> *, and no other kinds. But the intuition should still hold: 42 is an Int, and you can do Inty things with it like adding and subtracting. Int itself is not an Int; there is no such number as Int + Int. You may informally hear people say that Int is a Num, by which they mean that there is an instance of the Num type class for the type Int—this is not the same thing as saying that Int has kind Num. Int has kind "type", which in Haskell is spelled *.)

So isn't every informal "type" just a noun or a category? Do all types have the same kind? Why talk about kinds at all if they're so boring?

This is where the English analogy will get a little rocky, but bear with me: pretend that the word "owner" in English made no sense in isolation, without a description of the thing being owned. Pretend that if someone called you an "owner", that would make no sense to you at all; but if someone called you a "car owner", you could understand what they meant.

"Owner" does not have the same kind as "car", because you can talk about a car, but you can't talk about an owner in this made-up version of English. You can only talk about a "car owner". "Owner" only creates something of kind "noun" when it's applied to something that already has kind "noun", like "car". We would say that the kind of "owner" is "noun -> noun". "Owner" is like a function that takes a noun and produces from that a different noun; but it's not a noun itself.

Note that "car owner" is not a subtype of "car"! It's not a function that accepts or returns cars! It's just a completely separate type from "car". It describes values with two arms and two legs who at one point had a certain amount of money, and took that money to a dealership. It does not describe values that have four wheels and a paint job. Also note that "car owner" and "dog owner" are different types, and things you might want to do with one may not be applicable to the other.

(Likewise, when we say that Maybe has kind * -> * in Haskell, we mean that it's nonsensical (formally; informally we do it all the time) to talk about having "a Maybe". Instead, we can have a Maybe Int or a Maybe String, since those are things of kind *.)

So the whole point of talking about kinds at all is so that we can formalize our reasoning around words like "owner" and enforce that we only ever take values of types that have been "fully constructed" and aren't nonsensical.

Answer 4

As I understand it, a kind is a type of type.

That's right - so let's explore what that means. Int or Text are concrete types, but Maybe a is an abstract type. It won't become a concrete type until you decide what specific value you want for a for a particular variable (or value / expression / whatever) eg Maybe Text.

We say that Maybe a is a type constructor because it is like a function that takes a single concrete type (eg Text) and returns a concrete type (Maybe Text in this case). But other type constructors might take even more "input params" before they return a concrete type. eg Map k v needs to take two concrete types (eg Int and Text) before it can construct a concrete type (Map Int Text).

So, the Maybe a and List a type constructors have the same "signature" which we denote as * -> * (similarly to the Haskell function signature) because if you give them one concrete type they will spit out a concrete type. We call this the "kind" of the type and Maybe and List have the same kind.

The concrete types are said to have kind *, and our Map example is kind * -> * -> * because it takes two concrete types as input before it can output a concrete type.

You can see it is mostly just about the number of "parameters" that we pass in to the type constructor - but realise that we might also get type constructors nested inside type constructors, so we can end up with a kind that looks like * -> (* -> *) -> * for example.

If you are a Scala/Java dev, you may also find this explanation helpful: https://www.atlassian.com/blog/archives/scala-types-of-a-higher-kind