Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
This may be a very simple question.
But what is the difference between types and sorts?
My current understanding is that you have a type theory with type rules that give a notion of a well-typed statement but sorts are more basic, differentiating symbols into different sorts of symbols and introducing basic rules on function application etc.
Perhaps there is little difference, maybe they just come from different fields. But I can't seem to find a clear description of their relation.
The way I understand the difference is that the two concepts are used to give slightly different emphasis, but ultimately they are kind of the same thing. Since neither has a formal definition we cannot expect an exact answer without first limiting the scope to a particular understanding of "type" and "sort".
"Sort" is used when we want to say that there are several different, well, sorts of things that we need to distinguish. An example would be a theory of geometry with sorts "point" and "line".
"Type" is used when not only is there a need to distinguish different sorts of things, but proper attention is paid to the structure of the sorts/types themselves. Thus, typically we can form new types from old ones (products, sums, function types), we can have interesting relations between types (type equality, subtyping), etc. In contrast, one typically just specifies some sorts at the beginning, and then never pays much attention to the structure of the class of all sorts.
This at least is how I percieve the difference, other people may have different experiences.
Like Andrej says, neither term is completely formal, and talk about roughly the same kinds of things, so there isn't really a clear dividing line.
For myself, I think of the word "sort" as coming from model theory (as in multi-sorted first-order logic), and so I use the word "sort" to suggest that there is a set-theoretic interpretation of sets and inhabitants. The idea is that if $t$ is a term and $\sigma$ is a sort, then there are interpretations such that $t : \sigma$ implies $[\![t]\!] \in [\![\sigma]\!]$.
I do not make this suggestion when using the word "type". There are plenty of type theories which do not have simple set-theoretic interpretations, and many of them are highly relevant to programming. So if $e$ is an expression and $\tau$ is a type, then the judgement $e : \tau$ does not necessarily suggest any membership-style reading.
kindis the type of a type constructor or, less commonly, the type of a higher-order type operator. $\endgroup$