Going further one will need a word for "the kind of a kind", "the kind of a kind of a kind" and so on.

One solution is TypeInType, that is the type of a type is another type (not kind or something else). That's where Haskell is going with the work of adding Dependent Types to the language.

The problem with TypeInType is that it is logically inconsistent - it leads to Girard's paradox, analog to Russel's paradox in set theory.

The correct solution is type universes where every type lives in some type universe indexed by a natural number. For example terms are of type 'Type 1', 'Type 1' types are of type 'Type 2' and so on. The usual 'Type' is then just the first universe level 'Type 1' and 'Kind' is 'Type 2'.

Type universes is what most proof assistants employ, e.g. Agda, Coq, Lean. Idris uses TypeInType which is easier to use and there's no need to massage your program until all type universes type check but is logically inconsistent so one has to be careful to not reproduce Girard's paradox in some form or another.

Kinds are a distinct concept from types, and that concept needs a name, and it's best to choose a name where the intuitive meaning of the name aligns with the technical one (indeed Haskell attracts a lot of criticism when it uses names like "monad" that don't have a "fuzzy" meaning).

It goes even further: types-of-kinds are called "sorts", though in Haskell there's only one possible sort of kind.

There are only two hard problems in computer science, after all.

>There are only two hard problems in computer science, after all.

Including off-by-one errors, there are four.

Maybe we should add 'induction' to the list.

Naming and ??

(Computability?)

"There are only two hard things in Computer Science: cache invalidation and naming things." -- Phil Karlton

But I do like "Computability and naming things" better.

There are only two hard things in Computer Science: cache invalidation, naming things and off by one errors. -- Anonymous

Are you just saying you don't like the term "kind" or something else? The name has been used since the last century.

I suppose I wasn't clear.

In my experience, in computer science, "kind" is generally used in an informal way, whereas "type" is used to refer to the technical concept of type in type systems.

If Haskell gives a precise meaning to "kind", I'm going to have be careful which word I use to refer to the informal concept.

As I said, type theorists say things like "Type systems let us reify what kind of data we are dealing with".

I see. I think it's fine to overload an English word to have both a precise meaning or an informal one.

Objective-C called closures blocks because that is what they are called in Smalltalk.

Objective-C was modelled on Smalltalk.

The same happens with all sorts of collectiony words. You could have a set of things, or a group of them, or a variety or a category or a kind or a sort or a class or type. We're running out of collection words without formal definitions!

actually I’ve seen sort used for kinds of kinds in some PL papers that I’ve read. Not sure how official it is, some PL researchers I’ve talked to say that they don’t go higher than sorts.