<p>As I understand it, as a (value-level) function <code>f</code> that takes a value <code>x</code> of type <code>T</code> and returns a value <code>f x</code> of type <code>U</code> has type <code>T → U</code>, a type constructor <code>F</code> (a type-level function) that takes a type <code>T</code> and returns a type <code>F T</code> is said to have <em>kind</em> <code>* → *</code> or <code>Type → Type</code>, where <code>*</code> or <code>Type</code> is the type of &quot;small&quot; types, which are those types the values of which are not themselves types, unlike <code>Type</code>.</p>
<p>Some languages focussed on writing mathematical proofs take care to distinguish different levels of <code>Type</code>, to avoid ‘Girard's paradox’.
The function type <code>T → U</code> has type <code>Type</code>, whereas <code>Type</code> does not have type <code>Type</code> but has type <code>Type₁</code>, and <code>Type₁</code> has type <code>Type₂</code>, and so forth.
<a href="https://coq.inria.fr/distrib/V8.17.1/refman/language/core/sorts.html" rel="noreferrer">Coq</a> and <a href="https://agda.readthedocs.io/en/v2.6.3/language/sort-system.html" rel="noreferrer">Agda</a> call the types of types <em>sorts</em> and spell the type <code>Type</code> as <code>Set</code> and the types <code>Typeₙ</code> as <code>Type(n)</code> (in Coq) or <code>Setₙ</code> (in Agda). This sequence of types <code>Typeₙ</code> may be called a <em>universe hierarchy</em>.</p>
<p>I shall not be surprised if some of my above-stated understanding is wrong, as I have not studied any of this formally or systematically. If my understanding is not so wrong as to make my question meaningless, my question is:</p>
<p>As the type of value-level functions fits into the universe hierarchy, <strong>I wonder how kinds, the types of type-level functions, fit into the universe hierarchy.</strong> The things that fit into the universe hierarchy are <em>things that have types</em>, so <strong>what, if anything, is the type of a kind?</strong> If kinds do not have types, then do they have something <em>like</em> types? If so, do those kind-types form their own kind-universe hierarchy?</p>
<p>Google showed me pages about type universes and a few pages about kinds, but I see nothing that appears to discuss both together.</p>

<types><static-typing><type-theory>
How, if at all, do kinds fit into the type universe hierarchy?
CC BY-SA 4.0
2023-07-09T20:59:08.043Z
Obligatory mention of Swift where every Type is its own type, e.g. `Int.Type` is distinct from `String.Type`, and `type(of: Int.Type)` is `Int.Type.Type`, and so on...
Bbrk24
CC BY-SA 4.0
2023-07-09T23:28:37.740Z
I'm pretty sure there's no distinction between “types” and “kinds” in languages where `Type` has a type.
xigoi
CC BY-SA 4.0
2023-07-11T19:22:48.570Z
Strongly related: https://cs.stackexchange.com/questions/13285/universes-in-dependent-type-theory
Ryan Cavanaugh
CC BY-SA 4.0
2023-07-12T08:17:25.727Z
The answer would depend on your interpretation of types. If you have a first-order approach, i.e. types are a function, then kinds would also be elements of your universe and their type would be kind (creating an odd loop, yes). I'm not an expert on higher-order interpretation, so I won't provide an answer there.
feldentm
CC BY-SA 4.0
2023-07-25T04:48:23.503Z
[System U](https://en.wikipedia.org/wiki/System_U#Formal_definition) has `* : □ : △`, where `*` is the sort of *types* and `□` is the sort of *kinds*. Squint a bit and 
you can read that as `Type : Type₁ : Type₂ : ...` in more modern type theories.
Rufflewind
<h2>Sometimes kinds are a second universe level</h2>
<p>In languages with a strict separation between types and kinds, and where kinds themselves are not given sorts, it is possible to view them as equivalent to a language with precisely two universe levels.</p>
<p>Standard Haskell works this way. In Haskell 2010, <a href="https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-640004.1.1" rel="nofollow noreferrer">kinds have an exceptionally simple grammar</a>, which is sufficient to check kind well-formedness:</p>
<blockquote>
<p>To ensure that they are valid, type expressions are classified into different <em>kinds</em>, which take one of two possible forms:</p>
<ul>
<li><p>The symbol <span class="math-container">$*$</span> represents the kind of all nullary type constructors.</p>
</li>
<li><p>If <span class="math-container">$\kappa_1$</span> and <span class="math-container">$\kappa_2$</span> are kinds, then <span class="math-container">$\kappa_1 \to \kappa_2$</span> is the kind of types that take a type of kind <span class="math-container">$\kappa_1$</span> and return a type of kind <span class="math-container">$\kappa_2$</span>.</p>
</li>
</ul>
</blockquote>
<p>There is no separate language for classifying kinds because it is simply not necessary: there are no “kind constructors” other than <code>-&gt;</code>, and it is not possible for users to define new ones. Haskell 2010 also does not support polymorphic kinds, so there are no quantifiers. This is a straightforwardly two-level system.</p>
<h2>Sometimes kinds aren’t separate at all!</h2>
<p>However, not only is this notion of kinds not universal, it’s not even universal <em>within Haskell!</em> As of this writing, GHC is the only relevant implementation of Haskell available, and it departs quite dramatically from the simplicity of the Haskell 2010 kind system:</p>
<ul>
<li><p>GHC supports universal quantification in kinds via <a href="https://downloads.haskell.org/ghc/9.6.1/docs/users_guide/exts/poly_kinds.html#extension-PolyKinds" rel="nofollow noreferrer">the <code>PolyKinds</code> extension</a>.</p>
</li>
<li><p>GHC supports user-defined kind constructors via <a href="https://downloads.haskell.org/ghc/9.6.1/docs/users_guide/exts/data_kinds.html" rel="nofollow noreferrer">the <code>DataKinds</code> extension</a>.</p>
</li>
<li><p>Most radically, since a few years ago, <a href="https://downloads.haskell.org/ghc/9.6.1/docs/users_guide/exts/poly_kinds.html#extension-TypeInType" rel="nofollow noreferrer">GHC includes the universe-flouting <code>Type : Type</code> axiom</a>. This means <strong>there is no type–kind separation</strong>; they both belong to the same set.</p>
</li>
</ul>
<p>Type-in-type is known to be logically inconsistent for the reasons given in your question, but Haskell was already logically inconsistent, so including the type-in-type axiom does not change much in that respect.</p>
<h2>So what are kinds?</h2>
<p>The above might seem like wild variation in what a “kind” is, even within a single language. However, that is not really true: the word “kind” is simply used to describe the language that describes types. On its own, it does not mandate any particular logical interpretation.</p>
<p>Universe levels are primarily used in the context of dependently typed theorem provers, where they arise out of necessity. In those languages, logical consistency is absolutely necessary, yet the expression language of types and terms is unified. To avoid logical inconsistency, <em>something</em> must stratify the structure, and universe levels are a natural choice.</p>
<p>But the term “kind” is usually used in languages that are <em>not</em> dependently typed, so there is already a very strong type–term distinction, and there can be a similarly strong kind–type distinction. This may correspond to a set of logical universes, but it also might not; what matters is this syntactic relationship between terms, types, and kinds.</p>

CC BY-SA 4.0
2023-07-13T12:41:12.507Z
2024-11-23T06:24:52.977Z
2024-11-23T06:24:52.977Z
Alexis King
# How, if at all, do kinds fit into the type universe hierarchy?
Posted by: username_0 on 2023-07-09
As I understand it, as a (value-level) function `f` that takes a value `x` of type `T` and returns a value `f x` of type `U` has type `T → U`, a type constructor `F` (a type-level function) that takes a type `T` and returns a type `F T` is said to have *kind* `* → *` or `Type → Type`, where `*` or `Type` is the type of "small" types, which are those types the values of which are not themselves types, unlike `Type`.

Some languages focussed on writing mathematical proofs take care to distinguish different levels of `Type`, to avoid ‘Girard's paradox’.
The function type `T → U` has type `Type`, whereas `Type` does not have type `Type` but has type `Type₁`, and `Type₁` has type `Type₂`, and so forth.
[Coq](https://coq.inria.fr/distrib/V8.17.1/refman/language/core/sorts.html) and [Agda](https://agda.readthedocs.io/en/v2.6.3/language/sort-system.html) call the types of types *sorts* and spell the type `Type` as `Set` and the types `Typeₙ` as `Type(n)` (in Coq) or `Setₙ` (in Agda). This sequence of types `Typeₙ` may be called a *universe hierarchy*.

I shall not be surprised if some of my above-stated understanding is wrong, as I have not studied any of this formally or systematically. If my understanding is not so wrong as to make my question meaningless, my question is:

As the type of value-level functions fits into the universe hierarchy, **I wonder how kinds, the types of type-level functions, fit into the universe hierarchy.** The things that fit into the universe hierarchy are *things that have types*, so **what, if anything, is the type of a kind?** If kinds do not have types, then do they have something *like* types? If so, do those kind-types form their own kind-universe hierarchy?

Google showed me pages about type universes and a few pages about kinds, but I see nothing that appears to discuss both together.
**Tags:** types static-typing type-theory
> **Comments:**
> **username_1**: Obligatory mention of Swift where every Type is its own type, e.g. `Int.Type` is distinct from `String.Type`, and `type(of: Int.Type)` is `Int.Type.Type`, and so on...  
> **username_2**: I'm pretty sure there's no distinction between “types” and “kinds” in languages where `Type` has a type.  
> **username_3**: Strongly related: https://cs.stackexchange.com/questions/13285/universes-in-dependent-type-theory  
> **username_4**: The answer would depend on your interpretation of types. If you have a first-order approach, i.e. types are a function, then kinds would also be elements of your universe and their type would be kind (creating an odd loop, yes). I'm not an expert on higher-order interpretation, so I won't provide an answer there.  
> **username_5**: [System U](https://en.wikipedia.org/wiki/System_U#Formal_definition) has `* : □ : △`, where `*` is the sort of *types* and `□` is the sort of *kinds*. Squint a bit and 
you can read that as `Type : Type₁ : Type₂ : ...` in more modern type theories.  
---
## 1 answers
### Answer by username_6 on 2023-07-13. Score: 14 | Accepted answer
## Sometimes kinds are a second universe level

In languages with a strict separation between types and kinds, and where kinds themselves are not given sorts, it is possible to view them as equivalent to a language with precisely two universe levels.

Standard Haskell works this way. In Haskell 2010, [kinds have an exceptionally simple grammar](https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-640004.1.1), which is sufficient to check kind well-formedness:

> To ensure that they are valid, type expressions are classified into different *kinds*, which take one of two possible forms:
>
> * The symbol $\*$ represents the kind of all nullary type constructors.
> * If $\kappa\_1$ and $\kappa\_2$ are kinds, then $\kappa\_1 \to \kappa\_2$ is the kind of types that take a type of kind $\kappa\_1$ and return a type of kind $\kappa\_2$.

There is no separate language for classifying kinds because it is simply not necessary: there are no “kind constructors” other than `->`, and it is not possible for users to define new ones. Haskell 2010 also does not support polymorphic kinds, so there are no quantifiers. This is a straightforwardly two-level system.

## Sometimes kinds aren’t separate at all!

However, not only is this notion of kinds not universal, it’s not even universal *within Haskell!* As of this writing, GHC is the only relevant implementation of Haskell available, and it departs quite dramatically from the simplicity of the Haskell 2010 kind system:

* GHC supports universal quantification in kinds via [the `PolyKinds` extension](https://downloads.haskell.org/ghc/9.6.1/docs/users_guide/exts/poly_kinds.html#extension-PolyKinds).
* GHC supports user-defined kind constructors via [the `DataKinds` extension](https://downloads.haskell.org/ghc/9.6.1/docs/users_guide/exts/data_kinds.html).
* Most radically, since a few years ago, [GHC includes the universe-flouting `Type : Type` axiom](https://downloads.haskell.org/ghc/9.6.1/docs/users_guide/exts/poly_kinds.html#extension-TypeInType). This means **there is no type–kind separation**; they both belong to the same set.

Type-in-type is known to be logically inconsistent for the reasons given in your question, but Haskell was already logically inconsistent, so including the type-in-type axiom does not change much in that respect.

## So what are kinds?

The above might seem like wild variation in what a “kind” is, even within a single language. However, that is not really true: the word “kind” is simply used to describe the language that describes types. On its own, it does not mandate any particular logical interpretation.

Universe levels are primarily used in the context of dependently typed theorem provers, where they arise out of necessity. In those languages, logical consistency is absolutely necessary, yet the expression language of types and terms is unified. To avoid logical inconsistency, *something* must stratify the structure, and universe levels are a natural choice.

But the term “kind” is usually used in languages that are *not* dependently typed, so there is already a very strong type–term distinction, and there can be a similarly strong kind–type distinction. This may correspond to a set of logical universes, but it also might not; what matters is this syntactic relationship between terms, types, and kinds.
---
