What is the "type" of a kind?

Question

In Haskell the "types" of types are called Kinds, denoted as *. Such as in:

 Maybe :: * -> *
 Either :: * -> * -> *

I was wondering if there is any equivalent for the "types" of kinds in Haskell or other strongly typed languages?

Are they of any practical importance? Are there any cases where they turn out to be very useful?

Any reference to some material would be appreciated.

Answer 1

From GHC 8 onwards, as part of the march towards dependent types in Haskell, there's a new extension -XTypeInType that makes the "types" of kinds to be... types.

When TypeInType is on, there are just two levels in the language: terms and types. And the type level folds back on itself, so that the "type" (in Haskell terms, "kind") of a type is again a type.

Prelude> :set -XTypeInType
Prelude> import Data.Kind
Prelude Data.Kind> :k Int
Int :: *
Prelude Data.Kind> :k (*)
(*) :: *

Also Type becomes a synonym for *, the kind of types that have actual values at the term level:

Prelude Data.Kind> :k (Int :: *)
(Int :: *) :: *
Prelude Data.Kind> :k (Int :: Type)
(Int :: Type) :: *
Prelude Data.Kind> :k (Monad :: (Type -> Type) -> Constraint)
(Monad :: (Type -> Type) -> Constraint) :: (* -> *) -> Constraint

This lets you employ with kinds all the machinery that already exists for types, enriching Haskell's support for type-level shenanigans at the cost of being inconsistent from a logical perspective (which doesn't matter because Haskell is already "inconsistent" when considered as a proof system, for a host of other reasons).

Answer 2

In Haskell the "types" of types are called Kinds, denoted as *. Such as in:

This is not correct. * is the kind of types, i.e. of such type-level entities which represent a set^† of possible runtime values.

The term kind is a bit of a cludge. It's only needed because Haskell (for good reasons, no less!) has a clear distinction between compile time and run time. Values only exist at runtime, everything else only exists at compile time. In particular, the type of such values only exists at compile time.

Now, it's desirable to classify types as well, just as it is desirable to classify values in types. In principle, there is no reason not to consider types just like any other value and thus have types of types. This is pretty much the foundational idea of dependently-typed languages like Idris or Agda^¶.

In Haskell this doesn't quite work: because of the aforementioned runtime/compiletime distinction you can't throw types and values in one closed^‡ pot. Thus the concept of kinds: these are also types, but types of things that, unlike values, also exist at compile time like the kinds themselves do, not at runtime like values.

This means that there's no need to go yet another level up from kinds, because there's no earlier level than compile-time. (Unless you bring Template Haskell in the game; no idea if anybody has considered such issues yet.)

---

^†_{They aren't really sets, but kind of (pun not intended).}

^‡_{Closed in the sense: you can talk about types of types of types of... and never really need to invent anything new.}

^¶_{I understand that Agda still makes a distinction between types, type-types etc. (Set_2 and so on). But I believe this has more to do with the fact that Agda is a total language. I could be wrong here, though.}

Answer 3

Just as kinds classify types, so do sorts classify kinds.

http://jozefg.bitbucket.org/posts/2014-02-10-types-kinds-and-sorts.html