What are the issues with a set-like interpretation of quantifiers in type theory?

Question

In his answer to a question that tries to treat universal and existential quantifiers as intersections and unions of sets, Andrej Bauer says:

Forget the intersections and unions. People get this idea that ∀ and ∃ are like ⋂ and ⋃, which is the sort of thing the Polish school was doing a long time ago with Boolean algebras, but it's really not the way to go (definitely not in computer science).

and then introduces the traditional type-theoretic view of universal types as (collections of certain) functions and existential types as (collections of certain) pairs.

Question: what is wrong with the set-theoretic view? (Why was socumbersome asked to forget it?)

Further details: I ask because I'm interested in set-theoretic types (see eg. [0, 1]). where types are interpreted as collections of values, and the (set-theoretic) connectives union, intersection, and sometimes even negation are available. Interpreting quantifiers like unions and intersections (as in the linked question):

$$\forall x.T \overset{def}{:=} \bigcap_{S - type} T[x := S] $$ $$\exists x.T \overset{def}{:=} \bigcup_{S - type} T[x := S] $$

seems to me to be a natural extension of that view.

One (former?) issue I am aware of is that of dealing with cardinality of $D$ because of $D \cong D \to D$. But [0] says: "Systems which wish to reason about types as sets of values and who feature function types can quickly run into a problematic circularity in the metatheory and cardinality issues. Fortunately, these issues have been thoroughly addressed in prior work[28]" (the [28] is my [1]).

I even found an old paper[2] that I think (although I cannot claim much understanding) deals with the quantifiers that way. It, however, also syntactically restricts what type definitions are valid (on page 116):

So say $\sigma$ is (formally) contractive in t iff one of the following conditions hold:

1. $\sigma$ has one of the forms bool, int, $t'$ (with $t' \neq t$), $\sigma_1 \to \sigma_2$, $\sigma_1 \times \sigma_2$, or $\sigma_1 + \sigma_2$.
2. $\sigma$ has one of the forms $\sigma_1 \cap \sigma_2$ or $\sigma_1 \cup \sigma_2$ with both $\sigma_1$ and $\sigma_2$ contractive in t.
3. $\sigma$ has one of the forms $\forall t'.\sigma_1$, $\exists t'.\sigma_1$, or $\mu t'.\sigma_1$ with either $t' = t$ or $\sigma_1$ contractive in t.

Now we take TExp to be the set of well-formed type expressions where $\sigma$ is well formed iff one of the following conditions hold:

1. $\sigma$ is bool, int, or t.
2. $\sigma$ has one of the forms $\sigma_1 \to \sigma_2$, $\sigma_1 \times \sigma_2$, $\sigma_1 + \sigma_2$, $\sigma_1 \cap \sigma_2$, $\sigma_1 \cup \sigma_2$ with both $\sigma_1$ and $\sigma_2$ well-formed.
3. $\sigma$ has one of the forms $\forall t.\sigma_1$ or $\exists t.\sigma_1$ with $\sigma_1$ well formed.
4. $\sigma$ has the form $\mu t.\sigma_1$ with $\sigma_1$ well formed and contractive in t.

Below that it defines an interpretation function $\mathcal{T}\colon \mbox{TExp} \to \mbox{TEnv} \to \mathcal{P}(V)$, where $V$ is the space of all values (like booleans, naturals, functions of those, etc.) with the right isomorphisms.

This paper makes it harder for me to believe there is something wrong with the "set-theoretic" quantifiers, but maybe I just misunderstand something important.

0. Advanced Logical Type Systems for Untyped Languages - Andrew M. Kent; link
1. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types - Alain Frisch, Giuseppe Castagna, Véronique Benzaken; link
2. An ideal model for recursive polymorphic types - David MacQueen, Gordon Plotkin, Ravi Sethi; link

Answer 1

I think there may be a little nuance that can be applied to the situation, where 2 different possible hats may be applied, and which both are valid views of type systems.

View 1: Types are intrinsic

In this view, it makes no sense to talk about a program/term independently of its type. In addition

• $\forall$s and $\exists$s are really "forall"s and "exists" in the logical sense.
• Subject reduction is typically rather easy to prove (sort of)
• Typically types are unique: a term has only one type up to some equivalence relation.
• Typically type-checking is decidable.
• We care about termination and logical consistency: ideally there should be no term $\vdash t : \forall X.X$.
• There is (generally) no natural notion of subtype: if you want to restrict the possible values of a given type $T$, you need to form a $\Sigma$-type which contains a witness that the program behaves as expected (itself a program of some type). E.g. the type of positive integers $\Sigma x:\mathrm{Int}. x \geq 0$ is actually the type of pairs $(i, pos)$ where $pos$ is an inhabitant of the type $i\geq 0$.

Typically this is the view taken in dependent type theory, and I believe the view Andrej is promoting in his answer.

View 2: Types are behaviors

In this view, programs exist a priori without having an associated type, and the judgement $\vdash t : \sigma$ is taken to mean "program $t$ has behavior $\sigma$". This is generally the view taken whenever one mentions union or intersection types.

Some contrasts with the previous approach:

• Types are definitely not unique! Usually $\vdash t: \sigma$ for every possible behavior of $t$, e.g. $\lambda x. x$ has behavior $\mathrm{Int}\rightarrow \mathrm{Int}$ and also the incomparable behavior $\mathrm{Bool}\rightarrow\mathrm{Bool}$ etc.
• As a result, type checking and inference is usually undecidable.
• Subject reduction becomes quite subtle to prove.
• Normalization sometimes holds, but is less of a central topic.
• There is a subtle theory of subtyping where one can have $\mathrm{Nat}\subseteq\mathrm{Int}$ or even $\mathrm{Int}_{\geq 0}\subseteq\mathrm{Int}$ if the type system can express it. Terms need not carry witnesses that they belong in such or such type.
• There is some close connection with domain theory, which I do not know much about.

The papers you reference tend to adopt this second view. The two views are definitely not incompatible, but they tend to have different motivations and techniques.

I should finally note that there is a model of system $\mathrm{F}$ where $\Pi$s are interpreted as $\bigcap$, and this is generally used to prove normalization which is a "View 1" property. In some sense, this is a fluke: we're trying to reconcile these non-classical set theoretic views with some set theoretic model.

But it definitely "feels" like a "View 2" perspective. I'm not sure how to reconcile this, but there's probably something deep happening.

Answer 2

Cody's answer very nicely describes an important distinction. I would just like to point out a specific thing about the interpreation of $\forall$ as $\bigcap$.

A typical way to get $\forall$ interpreted as an intersection is to use a category of PERs on a partial combinatory algebra. Let $\mathbb{A}$ be an untyped model of computation, such as the untyped $\lambda$-calculus, or a universal domain, or Kleene's first partial combinatory algebra. The category $\mathsf{PER}(\mathbb{A})$ has as its objects partial equivalence relations (symmetric and transitive) on $\mathbb{A}$. It is provides a model for all sorts of type systems. In one of them, System F, we interpret $\forall$ as intersection: $$[\![ \forall X \,.\, \Phi(X) ]\!] = \bigcap_{R \in \mathsf{PER}(\mathbb{A})} [\![\Phi(R)]\!]. $$ One could say that this is a "set-theoretic" interpretation of a quantifier, except that it is not, because we used the category $\mathsf{PER}(\mathbb{A})$ rather than the category of sets. That is, for something to be called "set-theoretic" it has to use the structure of the category of sets in an essential way. I consider the above use of $\bigcap$ to be a coincidence: it just so happens that $\bigcap$ is the infimum operator in the complete lattice of $\mathsf{PER}(\mathbb{A})$. To my mind the nature of the model is order-theoretic, not set-theoretic.

In the comments I asked for an explanation of how the OP imagines the "set-like interpretation" of $\forall X \,.\, X \to X$ because I do not even understand what a "set-like interpretation of quantifiers" is supposed to mean. If we literally interpret $\forall$ as a class-sized intersection of sets, then $\forall X \,.\, X \to X$ is going to be empty, so far as $X \to X$ receives its usual meaning "the set of functional relations from $X$ to $X$". I still maintain that the problem with this question is not that people (and me in particular) are somehow "against" the set-theoretic interpretation – but that it's not clear at all what that would be, beyond what John Reynolds already wrote about it.