8
$\begingroup$

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 and Agda 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.

$\endgroup$
5
  • $\begingroup$ 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... $\endgroup$
    – Bbrk24
    Commented Jul 9, 2023 at 20:59
  • $\begingroup$ I'm pretty sure there's no distinction between “types” and “kinds” in languages where Type has a type. $\endgroup$
    – xigoi
    Commented Jul 9, 2023 at 23:28
  • $\begingroup$ Strongly related: cs.stackexchange.com/questions/13285/… $\endgroup$
    – Ryan Cavanaugh
    Commented Jul 11, 2023 at 19:22
  • $\begingroup$ 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. $\endgroup$
    – feldentm
    Commented Jul 12, 2023 at 8:17
  • 1
    $\begingroup$ System U 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. $\endgroup$
    – Rufflewind
    Commented Jul 25, 2023 at 4:48

1 Answer 1

Reset to default
11
$\begingroup$

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, 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:

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .