7

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?

  • 2
    You mean, like, God? Hmm... What constructs God, one might still wonder... – littleadv Nov 10 '11 at 19:45
  • I don't see that the following are true : (1): "A type is the type of a value." (2) "A type constructs a value" (3) "a kind constructs a type" – NoChance Nov 10 '11 at 19:45
  • 1
    You mean a programmer? – Karl Bielefeldt Nov 10 '11 at 19:50
4

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

5

In Haskell, we call the "types" of kinds sorts, though I don't know the nomenclature for other languages.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.