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 classifies type-level expressions. An ordinary type such as Int has kind Type (traditionally *), while a constructor such as Maybe has kind Type -> Type. Applying Maybe to Int is well-kinded because the argument's kind matches the constructor's domain. Kinds govern type formation, not just naming.[^{ref-45c0be30b696][}ref-d97a25f92e39]

Scope of Application¶

Haskell infers and checks kinds for type constructors. In the Cambridge System Fω example, the type-level operator \(F=\lambda\phi::(*\Rightarrow *\Rightarrow *).\phi\,1\,\mathrm{Bool}\) accepts the binary product \(\times\) and yields \(1\times\mathrm{Bool}::*\). That is a formal-calculus expression, not Haskell 98 surface syntax. Modern GHC supports polymorphic and promoted kinds, so the simple Type/arrow picture is introductory rather than exhaustive.[^{ref-45c0be30b696][}ref-d97a25f92e39][^ref-c27671aa04d6]

Clarity¶

Maybe Maybe is ill-kinded in the simple fixed-kind setting: the outer constructor expects Type, but the inner unapplied constructor has kind Type -> Type. A type constructor is the object classified; its kind is the classifier. A term value's ordinary type is a separate level of judgment.[^ref-45c0be30b696]

Manages Complexity¶

Kind rules check the shapes of potentially many nested type expressions with a small vocabulary of base and arrow kinds. They reject malformed constructor applications before reasoning about values, while allowing abstraction over constructors of a known kind.[^ref-c27671aa04d6]

Abstract Reasoning¶

For an application \(F\,A\), obtain \(F::K_1\Rightarrow K_2\) and \(A::K_1\). If the kinds match, the result has kind \(K_2\); if not, the expression fails the formation test. Use the kind rules of the specific language rather than assuming all theories share one fixed hierarchy.[^{ref-c27671aa04d6][}ref-d97a25f92e39]

Knowledge Transfer¶

The operator–argument compatibility test travels between Haskell implementations and System Fω. Their exact syntax, extensions and inference rules differ. “Kind” is a formal type-level classifier, not a generic synonym for category.[^{ref-45c0be30b696][}ref-c27671aa04d6]

[^ref-45c0be30b696]: Haskell 98 Language Report, declarations and kinds. [^ref-d97a25f92e39]: GHC User's Guide, Kind Polymorphism. [^ref-c27671aa04d6]: University of Cambridge System Fω lecture notes.

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