# Difference between Types and Sorts

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 meaning of terms depend of context. Can you give examples of the usage of types and sorts that you are asking about?: – Jeremy Jul 9 '13 at 12:52
• And then there are kinds. And classes. – lukstafi Jul 10 '13 at 21:14
• @Jeremy The answers have given me a clearer picture of the relation. I didn't have any examples where I was unclear of what was happening in a particular situation but was wondering if there was a significance in choosing a particular term. Thanks. – selig Jul 10 '13 at 22:22
• According to the Wikipedia entry on "Kind", a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator. – David Tonhofer Jan 19 '17 at 13:57

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.

• Just to clarify: the bracketed t and sigma means "the interpretation of"? In which case the "implies" would be better written as "means that"? – David Tonhofer Jan 19 '17 at 12:37
• I mean "if you have a derivation of $t : \sigma$, that implies the interpretation of $t$ is an element of the interpretation of $\sigma$". – Neel Krishnaswami Jan 19 '17 at 12:53