Types versus kinds and sorts

Question

In the context of logic, especially Higher‑Order‑Logic and Calculus‑of‑Construction, what is a kind and how does it relates to and differs from a type?

My raw guess if that a kind is the higher level type of a type. Is that it? If not, so what's a kind? If yes, is this as simple as it looks or are there more elaborated things to know about the relation between both?

Update: same question with sorts (or may be they are synonymous?).

Answer 1

Yes, your guess about kinds is correct. According to Types and Programming Languages, kinds are "the types of types".

From the same source:

[...] we introduce a system of kinds that classify type expressions according to their arity, just as arrow types tell us about the arities of terms. Kinds, then, are “the types of types.” In essence, the system of kinds is a copy of the simply typed lambda-calculus, “one level up.”

Answer 2

Will try to answer my own question (to be updated a future day).

Words in ML programmer's guide to ATS (cs.likai.org), suggests a sort is indeed a category above types:

Type definition assigns a static identifier to a static expression with the sort "type" […] The only difference is that typedef ensures that t will end up having the "type" sort, and stadef doesn't particularly care.

Since ATS is entirely based on an advanced type theory (close to CoC) and the author of the page is a CS professor, I believe the wording used in this document is meaningful.

Then later he adds more:

A type is one of the many sorts that a static expression or static identifier can be. Other sorts are:

• Ground sorts: int, bool, char, addr. They form the basis of dependent type indices.
• View, which are linear (in the sense of linear logic) propositions.
• Prop, which are classical propositions.
• Viewtype, which are linear types. It can be seen as a type combined with a view.

After this, I guess it's either an higher object level type (object type of an object type), or a meta‑language level type of an object level term. Discriminating between both, may be for a future day.

Update #1:

From the same source, later:

Notice that t@ype is a subsort of viewt@ype

As what's referred to as viewt@ype is at the object language level, sort is probably at object level too and is an object level category, above type, after the previous notes.

Confirmations from other sources would be nice. And this still do not answer the question about kinds.

Update #2:

During a talk in a mailing list, I get an answer, where there's a part relevant for this matter:

1. Applied Type System enforces a separation between the term, type, kind (sort) levels (in ATS2, there are only three such levels).

This suggests kind and sort are synonymous.