---
tag: B80MD5GX2D
kind: concept
name: Kind (type theory)
aliases: [higher-kind, higher-kinded, higher-kinded-type]
sources:
  - wikipedia: en:20627460@r1364770437
    locator: Kind (type theory)
    note: adopted
    mention: wikipedia://en/20627460
    sections: [Summary]
same_as:
  wikidata: Q6410497
  wikipedia: Kind (type theory)
inventory: [SWCSWG5N4G]
---

## Summary

In the area of mathematical logic and computer science known as type theory, a **kind** is the type of a type constructor or, less commonly, the type of a higher-order type operator (type constructor). A kind system is essentially a simply typed lambda calculus "one level up", endowed with a primitive type, usually denoted $*$ and called "type", which is the kind of any data type that does not need any type parameters.