Kind (Type Theory)¶

A type-level classifier that governs which types and type constructors can be formed or applied.

Version: v1 · 2026-10-03 · History
Domain-specific #: 13360
Domain group: Applied Sciences & Engineering
Origin domain: Computer Science & Software Engineering
Subdomains: Type Theory, Programming Language Theory → Computer Science & Software Engineering
Aliases: Type-theoretic kind, Kind of a type constructor

Core Idea¶

A kind is a classifier of type-level expressions. Ordinary values have types; types and type constructors can in turn be assigned kinds. In a simple kind language, \(\mathrm{Type}\) (traditionally \(*\)) is the kind of completed ordinary types, while \(\mathrm{Type}\to\mathrm{Type}\) is the kind of a constructor that takes an ordinary type and returns one. Thus Int has kind Type, Maybe has kind Type -> Type, and Maybe Int has kind Type. The point is not to add a decorative label: kinds make type-level application well-formed or ill-formed according to the operator and argument shapes.^[1]^[2]

System Fω makes the rule explicit in judgments: a type-level operator of kind \(K_1\Rightarrow K_2\) can be applied to an expression of kind \(K_1\), producing an expression of kind \(K_2\). Its type-level lambda abstraction has a corresponding kind-introduction rule. Haskell uses kind inference in an implemented language. These are two realizations of the same classification-and-formation pattern, not the same syntax or the same full theory.^[3]^[1]

Structural Signature¶

Sig role-phrases:

Type-level expression — The thing classified may be a completed type, an unapplied constructor or a higher type operator. A term value is classified by an ordinary type instead.^[1]^[3]
Kind vocabulary — A simple system has a base kind and arrow kinds; particular languages may add kind polymorphism or promoted kinds.^[1]^[2]
Kinding judgment — A context \(\Gamma\) supports a claim \(\Gamma\vdash A::K\), certifying that the type-level expression \(A\) has kind \(K\).^[3]
Application compatibility — If an operator expects a \(K_1\)-kind argument, an argument of some other kind cannot be substituted merely because it has a familiar name.^[3]
Language-specific extension boundary — Not every kind system is exactly the simple \(*\)/arrow fragment, and sorts or universes are not required for the basic identity.^[2]

Condensed: type-level expression + kind assignment + compatible kind-level application → well-formed type expression.

What It Is Not¶

Not an ordinary value's type. 3 :: Int is a term-level typing judgment; Int :: Type is a type-level kinding statement.^[2]
Not a type constructor itself. Live Type Constructor names an operator such as Maybe; the kind Type -> Type classifies that operator.^[1]
Not one mandatory * -> * notation. Haskell 98 writes *, while current GHC uses Type for ordinary lifted data types and supports richer kind forms.^[1]^[2]
Not always a simply typed lambda calculus in its entirety. The simple arrow-kind rules resemble that calculus at the type level, but kind polymorphism and dependent extensions can exceed the analogy.^[3]^[2]
Not proof that every type theory has a fixed type–kind–sort ladder. Additional classification levels or universes are system-specific.

Scope of Application¶

Kind checking is useful whenever type constructors can be partially applied, combined or abstracted over. The Haskell language report defines arrow kinds for constructors and says kind inference checks type expressions analogously to value-level type inference. GHC extends the language with polymorphic kinds and promoted data kinds; those extensions widen what can be classified without erasing the basic task of checking a type-level operator's input shape.^[1]^[2]

In formal calculi such as System Fω, type-level lambda terms can operate on types or other type operators. The kinding rules track these operations with introduction and elimination rules: abstraction constructs an arrow-kind operator, and application consumes an argument of the declared domain kind. This is more precise than the slogan “types have types,” because it states which expressions are legal.^[3]

Clarity¶

Maybe Int is well-kinded because Maybe :: Type -> Type receives Int :: Type. But Maybe Maybe is ill-kinded in the simple fixed-kind setting: the unapplied Maybe offered as the argument has kind Type -> Type, not the Type expected by the outer Maybe. A term-level type checker does not need to execute the program to find that mismatch; the type expression itself is malformed for this application.^[1]^[2]

Kinds are not synonymous with the number of parameters. Arity is often reflected in a chain of arrow kinds, but domain and codomain kinds matter too, particularly in higher-order or polymorphic settings. “Two arguments” is less informative than the full kinding rule that says what each argument must be.^[3]^[2]

Manages Complexity¶

Kinds compress potentially many malformed type-constructor applications into a small set of shape constraints. Rather than enumerate every illegal expression, a compiler or proof system assigns kinds and applies the same compatibility rule at each type-level application. This supports reusable abstractions over constructors while rejecting mismatches early.^[1]^[3]

The compression is not a claim that kind checking solves every type-system problem. A well-kinded type may still fail a separate type equality, subtyping or term-level typing requirement. A richer language may make kind inference itself more complex. The kind judgment answers a bounded question: is this type-level form admissible under the chosen calculus?^[3]^[2]

Abstract Reasoning¶

Given a proposed type expression, identify the kinds of its components. For an application \(F\,A\), find the declared or inferred kind of \(F\). If it has kind \(K_1\Rightarrow K_2\), check whether \(A\) has kind \(K_1\); then the result has kind \(K_2\). If the domain does not match, stop before discussing what values might inhabit the alleged result. For a type-level lambda, introduce a variable with an assumed kind and derive the body's result kind.^[3]

This move makes higher-kinded abstraction possible: a parameter may range over constructors rather than just completed types, provided its kind records what arguments it accepts. The exact permissible abstractions depend on the formal system. Modern GHC's kind polymorphism shows why the simple fixed-level ladder should be treated as a starting model, not a universal limit.^[2]

Knowledge Transfer¶

The classification rule transfers from Haskell's implemented type constructors to System Fω's formal type operators: in both, operators and arguments must have compatible kinds. What does not transfer without translation is concrete notation, built-in type universes or the precise inference algorithm. The old * and modern GHC Type spellings illustrate a change of language presentation, not a change in the basic reason for kind checking.^[1]^[2]^[3]

The broad idea of layered classification resembles many taxonomies, but this named entry is domain-specific because its carrier is a formal type-level language with formation judgments.

Examples¶

Haskell `Maybe Int`¶

The unary constructor Maybe expects a completed type. Int supplies one, so the application has a completed type's kind. This is the constructive side of kind checking.^[1]^[2]

Mapped back: expression = Maybe Int; operator kind = Type -> Type; argument kind = Type; result kind = Type.

System Fω type-level operator application¶

The Cambridge notes give the formal type-level expression \(F=\lambda\phi::(*\Rightarrow *\Rightarrow *).\phi\,1\,\mathrm{Bool}\). In the body, \(\phi\) takes two \(*\)-kind inputs; applying it to \(1::*\) leaves kind \(*\Rightarrow *\), then applying to \(\mathrm{Bool}::*\) gives kind \(*\). The abstraction therefore has kind \((*\Rightarrow *\Rightarrow *)\Rightarrow *\). The source's binary product operator \(\times\) has kind \(*\Rightarrow *\Rightarrow *\), so \(F\,\times\) is well-kinded with result kind \(*\) and reduces to \(1\times\mathrm{Bool}\). This is System Fω type-level lambda syntax, not a Haskell 98 source-language declaration.^[3]

Mapped back: expression = \(F\,\times\); input kind = \(*\Rightarrow *\Rightarrow *\); body kind = \(*\); generated operator kind = \((*\Rightarrow *\Rightarrow *)\Rightarrow *\); matched application result = \(1\times\mathrm{Bool}::*\).

Near miss: `Maybe Maybe`¶

In a fixed simple kind setting, the outer Maybe expects an argument of kind Type, but the unapplied inner Maybe has kind Type -> Type. The expression fails the kind application test even though both tokens denote familiar type constructors.^[1]

Structural Tensions¶

No intrinsic opposed-cost tension is established by this formal identity. Compatible kinds are a constitutive formation condition: \(F\,\times\) above is well-kinded, while offering an operator of the wrong kind would make the expression ill-formed, not pay a cost for expressivity. Haskell 98's simple kind fragment and GHC's richer kinds describe distinct language settings, not opposing pressures within one fixed rule system. Diagnostic: specify the calculus and derive the operator's domain kind and the argument's kind before asking any separate language-design question.^[3]^[2]

Structural–Framed Character¶

Kind (Type Theory) is a strongly structural formal classifier with language-specific framing. Kinding judgments and application rules are explicit: under a specified calculus, a mismatch is derivable rather than a matter of taste. The frame is which type language, built-in kinds and extensions are in force. The vocabulary arose in logic and programming-language theory; “kind” is technical here, not a generic everyday category. Human language designers choose the type constructors and formation rules, while a checker applies them consistently. Imported into another system, the analogy survives only if a comparable type-level classification judgment exists. Its character: formal in rule application and contingent in the chosen kind language.

Structural Core vs. Domain Accent¶

The skeleton is a classifier one level above the expressions it constrains. Here that relation is literal type-level kinding: formation judgments check constructor application against the kinds of arguments. The recorded Type System prerequisite supplies the rule environment, not a general above-expression classifier; Classification is related but is not asserted as this node's parent. If an analogous meta-level classifier occurs elsewhere, whether it forms one portable prime is a future-prime question, not evidence that this named kind identity travels there. Generic classification does not suffice; neither does the mere existence of constructors. This precise formation role keeps the entry domain-specific.

This entry presupposes Type System.

Type System is the accepted compositional prerequisite: a kind classifies type-level expressions under its formation judgments but is not the whole system. Type Constructor is classified by kinds, not their parent. Prime Classification is a broad analogy, and not every type system supports higher kinds.

Relationships to Other Abstractions¶

Current abstraction Kind (Type Theory) Domain-specific

Parents (1) — more general patterns this builds on

Kind (Type Theory) presupposes Type System Domain-specific

A kinding judgment presupposes a type system supplying type-level formation and application rules; kind is not the whole system.

Hierarchy paths (2) — routes to 2 parentless roots

Kind (Type Theory) → Type System → Classification

Show alternative path (1)

Neighborhood in Abstraction Space¶

Kind (Type Theory) sits in a moderately populated region (59^th percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.

Family — Type Systems & Functional Constructs (18 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With¶

A type, a kind and a type constructor play different roles: types classify terms; kinds classify type-level expressions; constructors form type expressions and have kinds. Some richer systems blur a rigid syntactic distinction between types and kinds, but they still have formation judgments that determine whether type-level application is valid.^[1]^[2]

References¶

[1] Haskell 98 Language Report, declarations and kind inference, §§4.1.1, 4.6. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m

[2] Glasgow Haskell Compiler User's Guide, Kind Polymorphism, official language documentation. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o

[3] University of Cambridge System Fω lecture notes, §1.5 kind introduction and elimination rules. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m