What exactly is the kind "*" in Haskell?

Question

In Haskell, (value-level) expressions are classified into types, which can be notated with :: like so: 3 :: Int, "Hello" :: String, (+ 1) :: Num a => a -> a. Similarly, types are classified into kinds. In GHCi, you can inspect the kind of a type expression using the command :kind or :k:

> :k Int
Int :: *
> :k Maybe
Maybe :: * -> *
> :k Either
Either :: * -> * -> *
> :k Num
Num :: * -> Constraint
> :k Monad
Monad :: (* -> *) -> Constraint

There are definitions floating around that * is the kind of "concrete types" or "values" or "runtime values." See, for example, Learn You A Haskell. How true is that? We've had a few questions about kinds that address the topic in passing, but it'd be nice to have a canonical and precise explanation of *.

What exactly does * mean? And how does it relate to other more complex kinds?

Also, do the DataKinds or PolyKinds extensions change the answer?

Answer 1

First off, * is not a wildcard! It's also typically pronounced "star."

Bleeding edge note: There is as of Feb. 2015 a proposal to simplify GHC's subkind system (in 7.12 or later). That page contains a good discussion of the GHC 7.8/7.10 story. Looking forward, GHC may drop the distinction between types and kinds, with * :: *. See Weirich, Hsu, and Eisenberg, System FC with Explicit Kind Equality.

The Standard: A description of type expressions.

The Haskell 98 report defines * in this context as:

The symbol * represents the kind of all nullary type constructors.

In this context, "nullary" simply means that the constructor takes no parameters. Either is binary; it can be applied to two parameters: Either a b. Maybe is unary; it can be applied to one parameter: Maybe a. Int is nullary; it can be applied to no parameters.

This definition is a little bit incomplete on its own. An expression containing a fully-applied unary, binary, etc. type constructor also has kind *, e.g. Maybe Int :: *.

In GHC: Something that contains values?

If we poke around the GHC documentation, we get something closer to the "can contain a runtime value" definition. The GHC Commentary page "Kinds" states that "'*' is the kind of boxed values. Things like Int and Maybe Float have kind *." The GHC user's guide for version 7.4.1, on the other hand, stated that * is the kind of "lifted types". (That passage wasn't retained when the section was revised for PolyKinds.)

Boxed values and lifted types are a bit different. According to the GHC Commentary page "TypeType",

A type is unboxed iff its representation is other than a pointer. Unboxed types are also unlifted.

A type is lifted iff it has bottom as an element. Closures always have lifted types: i.e. any let-bound identifier in Core must have a lifted type. Operationally, a lifted object is one that can be entered. Only lifted types may be unified with a type variable.

So ByteArray#, the type of raw blocks of memory, is boxed because it is represented as a pointer, but unlifted because bottom is not an element.

> undefined :: ByteArray#
Error: Kind incompatibility when matching types:
   a0 :: *
   ByteArray# :: #

Therefore it appears that the old User's Guide definition is more accurate than the GHC Commentary one: * is the kind of lifted types. (And, conversely, # is the kind of unlifted types.)

Note that if types of kind * are always lifted, for any type t :: * you can construct a "value" of sorts with undefined :: t or some other mechanism to create bottom. Therefore even "logically uninhabited" types like Void can have a value, i.e. bottom.

So it seems that, yes, * represents the kind of types that can contain runtime values, if undefined is your idea of a runtime value. (Which isn't a totally crazy idea, I don't think.)

GHC Extensions?

There are several extensions which liven up the kind system a bit. Some of these are mundane: KindSignatures lets us write kind annotations, like type annotations.

ConstraintKinds adds the kind Constraint, which is, roughly, the kind of the left-hand side of =>.

DataKinds lets us introduce new kinds besides * and #, just as we can introduce new types with data, newtype, and type.

With DataKinds every data declaration (terms and conditions may apply) generates a promoted kind declaration. So

 data Bool = True | False

introduces the usual value constructor and type name; additionally, it produces a new kind, Bool, and two types: True :: Bool and False :: Bool.

PolyKinds introduces kind variables. This just a way to say "for any kind k" just like we say "for any type t" at the type level. As regards our friend * and whether it still means "types with values", I suppose you could say a type t :: k where k is a kind variable could contain values, if k ~ * or k ~ #.

Answer 2

In the most basic form of the kind language, where there are only the kind * and the kind constructor ->, then * is the kind of things that can stand in a type-of relationship to values; nothing with a different kind can be a type of values.

Types exist to classify values. All values with the same type are interchangeable for the purpose of type-checking, so the type checker only has to care about types, not specific values. So we have the "value level" where all the actual values live, and the "type level" where their types live. The "type-of" relationship forms links between the two levels, with a single type being the type of (usually) many values. Haskell makes these two levels quite explicit; it's why you can have declarations like data Foo = Foo Int Chat Bool where you've declared a type-level thing Foo (a type with kind *) and a value-level thing Foo (a constructor with type Int -> Char -> Bool -> Foo). The two Foos involved simply refer to different entities on different levels, and Haskell separates these so completely that it can always tell what level you're referring to and thus can allow (sometimes confusingly) things on the different levels to have the same name.

But as soon as we introduce types that themselves have structure (like Maybe Int, which is a type constructor Maybe applied to a type Int), then we have things that exist at the type level which do not actually stand in a type-of relationship to any values. There are no values whose type is just Maybe, only values with type Maybe Int (and Maybe Bool, Maybe (), even Maybe Void, etc). So we need to classify our type-level things for the same reason we need to classify our values; only certain type-expressions actually represent something that can be the type of values, but many of them work interchangeably for the purpose of "kind-checking" (whether it's a correct type for the value-level thing it's declared to be the type of is a problem for a different level).¹

So * (which is often stated to be pronounced "type") is the basic kind; it's the kind of all type-level things that can be stated to be the type of values. Int has values; therefore its type is *. Maybe does not have values, but it takes an argument and produces a type that has values; this gets us a kind like ___ -> *. We can fill in the blank by observing that Maybe's argument is used as the type of the value appearing in Just a, so its argument must also be a type of values (with kind *), and so Maybe must have kind * -> *. And so on.

When you're dealing with kinds that only involve stars and arrows, then only type-expressions of kind * are types of values. Any other kind (e.g. * -> (* -> * -> *) -> (* -> *)) only contains other "type-level entities" that are not actual types that contain values.

PolyKinds, as I understand it, doesn't really change this picture at all. It just allows you to make polymorphic declarations at the kind-level, meaning it adds variables to our kind language (in addition to stars and arrows). So now I can contemplate type-level things of kind k -> *; this could be instantiated to work as either kind * -> * or (* -> *) -> * or (* -> (* -> *)) -> *. We've gained exactly the same kind of power as having (a -> b) -> [a] -> [b] at the type level gained us; we can write one map function with a type that contains variables, instead of having to write every possible map function separately. But there's still only one kind that contains type-level things that are the types of values: *.

DataKinds also introduces new things to the kind language. Effectively what it does though is to let us declare arbitrary new kinds, which contain new type-level entities (just as ordinary data declarations allow us to declare arbitrary new types, which contain new value-level entities). But it doesn't let us declare things with a correspondence of entities across all 3 levels; if I have data Nat :: Z | S Nat and use DataKinds to lift it to the kind level, then we have two different things named Nat that exist on the type level (as the type of value-level Z, S Z, S (S Z), etc), and at the kind level (as the kind of type-level Z, S Z, S (S Z)). The type-level Z is not the type of any values though; the value Z inhabits the type-level Nat (which in turn is of kind *), not the type-level Z. So DataKinds adds new user defined things to the kind language, which can be the kind of new user-defined things at the type level, but it remains the case that the only type-level things that can be the types of values are of kind *.

The only addition to the kind language that I'm aware of which truly does change this are the kinds mentioned in @ChristianConkle's answer, such as # (I believe there are a couple more now too? I'm not really terribly knowledgeable about "low level" types such as ByteArray#). These are the kinds of types that have values that GHC needs to know to treat differently (such as not assuming they can be boxed and lazily evaluated), even when polymorphic functions are involved, so we can't just attach the knowledge that they need to be treated differently to these values' types, or it would be lost when calling polymorphic functions on them.

---

¹ The word "type" can thus be a little confusing. Sometimes it is used to refer to things that actually stand in a type-of relationship to things on the value level (this is the interpretation used when people say "Maybe is not a type, it's a type-constructor"). And sometimes it's used to refer to anything that exists at the type-level (under this interpretation Maybe is in fact a type). In this post I'm trying to very explicitly refer to "type-level things" rather than use "type" as a short-hand.

Answer 3

For beginners that are trying to learn about kinds (you can think of them as the type of a type) I recommend this chapter of the Learn you a Haskell book.

I personally think of kinds in this way:

You have concrete types, e.g. Int, Bool,String, [Int], Maybe Int or Either Int String.

All of these have the kind *. Why? Because they can't take any more types as a parameter; an Int, is an Int; a Maybe Int is a Maybe Int. What about Maybe or [] or Either, though?

When you say Maybe, you do not have a concrete type, because you didn't specify its parameter. Maybe Int or Maybe String are different but both have a * kind, but Maybe is waiting for a type of kind * to return a kind *. To clarify, let's look at what GHCI's :kind command can tell us:

Prelude> :kind Maybe Int
Maybe Int :: *
Prelude> :kind Maybe
Maybe :: * -> *

With lists it's the same:

Prelude> :k [String]
[String] :: *
Prelude> :k []
[] :: * -> *

What about Either?

Prelude> :k Either Int String
Either Int String :: *
Prelude> :k Either Int
Either Int :: * -> *

You could think of intuitively think of Either as a function that takes parameters, but the parameters are types:

Prelude> :k Either Int
Either Int :: * -> *

means Either Int is waiting for a type parameter.