26
$\begingroup$

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?

$\endgroup$
  • 6
    $\begingroup$ I just came here from the post on Stack Overflow that led to this discussion. I'm not sure I'm qualified to answer in detail - but you're definitely being way too literal about the terms "type" and "kind", in trying to relate them to their meaning in English (where indeed they are synonyms). You should treat them as technical terms. "Type" is well-understood by all programmers, I assume, because the concept is vital to every language, even weakly-typed ones like Javascript, "Kind" is a technical term used in Haskell for the "type of a type". That's really all there is to it. $\endgroup$ – Robin Zigmond Jul 2 at 22:22
  • 2
    $\begingroup$ @RobinZigmond: you're right in that these are techniical terms, but they are used more widely than just in Haskell. Maybe backlink to the Stack Overflow discussion that begat this question? $\endgroup$ – Andrej Bauer Jul 2 at 22:28
  • $\begingroup$ @AndrejBauer I never said that they weren't used outside of Haskell, certainly "type" is used in essentially every language, as I said. I've never actually come across "kind" outside Haskell, but then Haskell is the only functional language I know at all, and I was careful not to say the term isn't used elsewhere, just that it is used in that way in Haskell. (And the link, as you request, is here) $\endgroup$ – Robin Zigmond Jul 2 at 22:32
  • $\begingroup$ ML-family languages have kinds too, for instance Standard ML and OCaml. They're not exposed explicitly by that name, I think. They are manifested as signatures, and their elements are called structures. $\endgroup$ – Andrej Bauer Jul 3 at 9:23
  • 1
    $\begingroup$ A more accurate English analogy is Ford is a type of car and car is a type of vehicles but both car-types and vehicle-types are of the same kind: nouns. Whereas red is a type of car color and RPM is a type of car performance metrics and both are of the same kind: adjectives. $\endgroup$ – slebetman Jul 6 at 2:55
32
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ If "types and kinds are really the same thing", then the type of type is just type itself, and there would be no need at all for kind. So what precisely is the distinction? $\endgroup$ – user21820 Jul 3 at 12:11
  • 1
    $\begingroup$ @user21820, I added a note to the end that might address this. Short answer: there isn't really a distinction in modern GHC Haskell. $\endgroup$ – K. A. Buhr Jul 3 at 16:53
  • 1
    $\begingroup$ This is a great answer - thanks very much for sharing. It's well written and introduces concepts gradually - as someone who hasn't written Haskell for a few years, this is very much appreciated! $\endgroup$ – ultrafez Jul 3 at 19:34
  • $\begingroup$ @K.A.Buhr: Thanks for that added bit! $\endgroup$ – user21820 Jul 4 at 17:25
19
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ I don't think (GHC) Haskell has any concept of universes. Type :: Type is an axiom. The distinction between "type" and "kind" is entirely in human language, in that case. True has a type, Bool, and Bool has a type Type, which itself has type Type. Sometimes we call a type a kind, to emphasize that it's the type of a type-level entity, but, in Haskell, it's still just a type. In a system where universes actually exist, like Coq, then "type" may refer to one universe and "kind" to another, but then we usually want infinitely many universes. $\endgroup$ – HTNW Jul 3 at 8:15
  • 1
    $\begingroup$ The distinction is not just "human language", it's a formal distinction in the underlying type system. It's quite possible to have both Type :: Type and a distinction between types and kinds. Also, what piece of code demonstrates Type :: Type in Haskell? $\endgroup$ – Andrej Bauer Jul 3 at 8:26
  • 1
    $\begingroup$ I should also say that * in Haskell is a universe of a sorts. They just don't call it that. $\endgroup$ – Andrej Bauer Jul 3 at 8:34
  • 3
    $\begingroup$ @AndrejBauer Type from Data.Kinds and * should be synonyms. Initially we only had * as a primitive, while nowadays that is internally defined as GHC.Types.Type in the internal module GHC.Types, in turn defined as type Type = TYPE LiftedRep. I think TYPE is the real primitive, providing a family of kinds (lifted types, unboxed types, ...). Most of the "inelegant" complexity here is to support some low-level optimizations, and not for actual type theoretic reasons. $\endgroup$ – chi Jul 3 at 10:24
  • 1
    $\begingroup$ I'll try to summarize. If v is a value, then it has a type: v :: T. If T is a type, then it has a type: T :: K. The type of type is called its kind. Types that look like TYPE rep may be called sorts, though the word is uncommon. Iff T :: TYPE rep is T is allowed to appear on the RHS of a ::. The word "kind" has nuance to it: K in T :: K is a kind, but not in v :: K, though it's the same K. We could define "K is a kind if its kind is a sort" aka "kinds are on the RHS of ::", but that doesn't capture the usage correctly. Therefore my "human distinction" position. $\endgroup$ – HTNW Jul 3 at 11:03
5
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ I'm not saying that your analogy is wrong, but I think it may cause confusion. Dijkstra has some words about analogies. Google "On the cruelty of really teaching computing science". $\endgroup$ – Rafael Castro Jul 2 at 23:08
  • $\begingroup$ I mean, there are car analogies, and then there are car analogies. I don't think that highlighting the implicit type structure in a natural language (which, admittedly, I did stretch in the second half) as a way of explaining a formal type system is the same sort of teaching-through-analogy as talking about what a program "wants" to do. $\endgroup$ – user11228628 Jul 2 at 23:43
1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ This is not correct. In Haskell, we distinguish between Maybe a, a synonym for forall a. Maybe a, a polymorphic type of kind *, and Maybe, a monomorphic type of kind * -> *. $\endgroup$ – b0fh Jul 5 at 8:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.