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?
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: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 likeInt
andMaybe 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 forPolyKinds
.)Boxed values and lifted types are a bit different. According to the GHC Commentary page "TypeType",
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.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 typet :: *
you can construct a "value" of sorts withundefined :: t
or some other mechanism to create bottom. Therefore even "logically uninhabited" types likeVoid
can have a value, i.e. bottom.So it seems that, yes,
*
represents the kind of types that can contain runtime values, ifundefined
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 kindConstraint
, 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 withdata
,newtype
, andtype
.With
DataKinds
everydata
declaration (terms and conditions may apply) generates a promoted kind declaration. Sointroduces the usual value constructor and type name; additionally, it produces a new kind,
Bool
, and two types:True :: Bool
andFalse :: Bool
.PolyKinds
introduces kind variables. This just a way to say "for any kindk
" just like we say "for any typet
" at the type level. As regards our friend*
and whether it still means "types with values", I suppose you could say a typet :: k
wherek
is a kind variable could contain values, ifk ~ *
ork ~ #
.