Software Engineering Stack Exchange is a question and answer site for professionals, academics, and students working within the systems development life cycle. It only takes a minute to sign up.
Sign up to join this community
We all know what a value is. A type is the type of a value. A kind is (loosely) the type of a type. A type constructs a value; a kind constructs a type. So what is the type of a kind, a thing that constructs kinds?
Is there such a thing? Does it have a name? Is it useful?
According to the basic Wikipedia entry about kinds "a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator". So I understand that to mean the type of a kind is a kind and it's kinds all the way down (which makes sense - otherwise we would need an infinite number of names, one for each meta-type(i)).
From the same reference:
"(* => *) => * is the kind of a higher-order type operator from unary type constructors to proper types. These are very seldom encountered, even in programming language theory, but see Pierce (2002), chapter 32 for an application."
would seem to indicate it has limited but non-zero usefulness.
Not a great answer, but hopefully it will stop the "not a real question" close votes until someone who, say, implemented a Haskell compiler and really knows what he's talking about comes along...
In Haskell, we call the "types" of kinds sorts, though I don't know the nomenclature for other languages.
