# Difference between "sort" and "universe"

A very basic question. As title, what is the difference between "sort" and "universe" in type theory? Are they interchangable? Or are there only finite number of sorts, but infinite universes?

• The universe is a set of objects. Each object has a type ("sort"). Feb 27, 2016 at 14:19

Sort is (typically, though see Pure Type Systems) a meta-level concept and universes are an internalization of a particular case of a sort. The second chapter of Bart Jacobs' thesis covers a fairly general case of how sorts interact with a language. I'll be roughly following that.

I'll use the terminology $T$ is a type of sort $s$ if $T : s$ and $e$ is a term of type $T$ if $e : T$, so terms are always "grandchildren" of some sort, and types are always "children". $s$ is a sort if we can introduce variables of a type of sort $s$ into the context, i.e. $$\frac{\Gamma\vdash A : s}{\Gamma, x:A\vdash x:A}$$

If there were no dependencies between sorts, we could almost say a sort was an index into a collection of contexts, which leads to the notion of dependencies between sorts. We say $s_2$ depends on $s_1$ when types of sort $s_2$ can contain terms of sort $s_1$, i.e. if $$\frac{}{\Gamma\vdash A:s_1\qquad \Gamma,x:A\vdash B:s_2}$$ then it can be the case that $x$ occurs free in $B$. Without the dependency it would necessarily be the case that $x$ was not free in $B$.

That's all that is required to be a sort. Many additional features can be specified such as the existence of function types of sort $s$ built out of other types of sort $s$. One feature we can add (called axioms in Jacobs' thesis), is the fact that one sort is a type of another sort, i.e. $s_1 : s_2$. This internalizes the types of sort $s_1$ as terms of sort $s_2$. If we want to embed $s_1$ into $s_2$ so that terms of $s_1$ are terms of $s_2$, we can add what Jacobs calls an $(s_1,s_2)$-inclusion.

A universe is then a sort that is closed under all the operations in the language. A hierarchy of universes means that we further internalize the types of every universe and have an embedding of each universe into (at least) the next higher universe. Closure typically includes the following rule arising from dependent products: $$\frac{\Gamma\vdash A:\mathbb{U}_n\qquad\Gamma,x:A\vdash B:\mathbb{U}_n}{\Gamma\vdash(\Pi x\!:\!A.B) : \mathbb{U}_n}$$ For this to be interesting, $x$ has to occur free in $B$ meaning $\mathbb{U}_n$ depends on $\mathbb{U}_n$. Cycles of dependencies between sorts are characteristic of dependently typed languages.

So a (hierarchy of) universe(s) is a (hierarchy of) sort(s) with a variety of additional features many of which imply additional dependencies. For contrast, we can consider sorts (potentially in addition to a hierarchy of universes) that aren't universes (or at least aren't the universe, i.e. we could have multiple universe hierarchies). One example is separating compile-time calculation from run-time calculation as in Higher-order ML. In this we'd have a sort that represents compile-time terms in addition to a sort for run-time terms and a dependency allowing run-time terms to depend on compile-time terms. Another example is Cloud Haskell's Static type constructor. We can view it as part of a $(\square,*)$-inclusion where sort $\square$ classifies "static" terms which are terms which only depend on terms bound at the top level.

• So, are sorts in PTS actually universes?
– 盛安安
Feb 27, 2016 at 15:17
• Which one of Bart Jacobs' theses are you referring to? There are a lot of them in your link.
– 盛安安
Feb 27, 2016 at 15:21
• His 1991 PhD thesis "Categorical Type Theory". The term "universe" is not usually used in type theory outside of dependently typed contexts. Insofar as universes imply or require some form of dependent typing, sorts in pure type systems need not be universes. In particular, a sort in a PTS need not support quantifying over itself (or support quantification at all for that matter). Feb 27, 2016 at 16:07