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

<p>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]\!]$. </p>

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

CC BY-SA 3.0
2017-01-19T12:37:58.450Z
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
CC BY-SA 3.0
2017-01-19T12:53:26.147Z
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
CC BY-SA 3.0
2013-07-10T11:01:40.220Z
2013-07-10T11:01:40.220Z
Neel Krishnaswami
<p>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".</p>

<p>"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".</p>

<p>"Type" is used when not only is there a need to distinguish different sorts of things, but proper attention is paid to the <em>structure</em> 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.</p>

<p>This at least is how I percieve the difference, other people may have different experiences.</p>

CC BY-SA 3.0
2013-07-09T12:14:05.273Z
2013-07-09T12:14:05.273Z
Andrej Bauer
<p>This may be a very simple question.</p>

<p>But what is the difference between types and sorts?</p>

<p>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 <em>sorts</em> of symbols and introducing basic rules on function application etc.</p>

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

CC BY-SA 3.0
2013-07-09T12:52:01.100Z
The meaning of terms depend of context. Can you give examples of the usage of types and sorts that you are asking about?:
J.y B.y
CC BY-SA 3.0
2013-07-10T21:14:11.267Z
And then there are kinds. And classes.
lukstafi
CC BY-SA 3.0
2013-07-10T22:22:54.783Z
@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
CC BY-SA 3.0
2017-01-19T13:57:44.283Z
According to [the Wikipedia entry on "Kind"](https://en.wikipedia.org/wiki/Kind_(type_theory)), a `kind` is the type of a [type constructor](https://en.wikipedia.org/wiki/Type_constructor) or, less commonly, the type of a higher-order type operator.
David Tonhofer
<type-theory>
Difference between Types and Sorts
selig
# Difference between Types and Sorts

(Asked by: username_0 on 2013-07-09)

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.

**Tags:** type-theory

> **Comments:**
> **username_1**: The meaning of terms depend of context. Can you give examples of the usage of types and sorts that you are asking about?:  
> **username_2**: And then there are kinds. And classes.  
> **username_0**: @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.  
> **username_3**: According to [the Wikipedia entry on "Kind"](https://en.wikipedia.org/wiki/Kind_(type_theory)), a `kind` is the type of a [type constructor](https://en.wikipedia.org/wiki/Type_constructor) or, less commonly, the type of a higher-order type operator.  

---

## 2 answers

### Answer by username_5 on 2013-07-09. Score: 21 | Accepted answer

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.


---

### Answer by username_4 on 2013-07-10. Score: 10

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.

> **Comments:**
> **username_3**: Just to clarify: the bracketed t and sigma means "the interpretation of"? In which case the "implies" would be better written as "means that"?  
> **username_4**: I mean "if you have a derivation of $t : \sigma$, that implies the interpretation of $t$ is an element of the interpretation of $\sigma$".  

---

