<p>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.</p>
<p><strong>View 1: Types are <em>intrinsic</em></strong></p>
<p>In this view, it makes no sense to talk about a program/term independently of its type. In addition</p>
<ul>
<li><span class="math-container">$\forall$</span>s and <span class="math-container">$\exists$</span>s are really &quot;forall&quot;s and &quot;exists&quot; in the logical sense.</li>
<li>Subject reduction is typically rather easy to prove (sort of)</li>
<li>Typically types are <em>unique</em>: a term has only one type up to some equivalence relation.</li>
<li>Typically type-checking is decidable.</li>
<li>We care about termination and logical consistency: ideally there should be no term <span class="math-container">$\vdash t : \forall X.X$</span>.</li>
<li>There is (generally) no natural notion of <em>subtype</em>: if you want to restrict the possible values of a given type <span class="math-container">$T$</span>, you need to form a <span class="math-container">$\Sigma$</span>-type which contains a <em>witness</em> that the program behaves as expected (itself a program of some type). E.g. the type of positive integers <span class="math-container">$\Sigma x:\mathrm{Int}. x \geq 0$</span> is actually the type of pairs <span class="math-container">$(i, pos)$</span> where <span class="math-container">$pos$</span> is an inhabitant of the type <span class="math-container">$i\geq 0$</span>.</li>
</ul>
<p>Typically this is the view taken in dependent type theory, and I believe the view Andrej is promoting in his answer.</p>
<p><strong>View 2: Types are <em>behaviors</em></strong></p>
<p>In this view, programs exist <em>a priori</em> without having an associated type, and the judgement <span class="math-container">$\vdash t : \sigma$</span> is taken to mean &quot;program <span class="math-container">$t$</span> has <em>behavior</em> <span class="math-container">$\sigma$</span>&quot;. This is generally the view taken whenever one mentions union or intersection types.</p>
<p>Some contrasts with the previous approach:</p>
<ul>
<li>Types are definitely not unique! Usually <span class="math-container">$\vdash t: \sigma$</span> for every possible behavior of <span class="math-container">$t$</span>, e.g. <span class="math-container">$\lambda x. x$</span> has behavior <span class="math-container">$\mathrm{Int}\rightarrow \mathrm{Int}$</span> and also the incomparable behavior <span class="math-container">$\mathrm{Bool}\rightarrow\mathrm{Bool}$</span> etc.</li>
<li>As a result, type checking and inference is usually undecidable.</li>
<li>Subject reduction becomes quite subtle to prove.</li>
<li>Normalization sometimes holds, but is less of a central topic.</li>
<li>There is a subtle theory of subtyping where one can have <span class="math-container">$\mathrm{Nat}\subseteq\mathrm{Int}$</span> or even <span class="math-container">$\mathrm{Int}_{\geq 0}\subseteq\mathrm{Int}$</span> if the type system can express it. Terms need not carry witnesses that they belong in such or such type.</li>
<li>There is some close connection with domain theory, which I do not know much about.</li>
</ul>
<p>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.</p>
<p>I should finally note that there is a model of system <span class="math-container">$\mathrm{F}$</span> where <span class="math-container">$\Pi$</span>s are interpreted as <span class="math-container">$\bigcap$</span>, and this is generally used to prove normalization which is a &quot;View 1&quot; property. In some sense, this is a fluke: we're trying to reconcile these non-classical set theoretic views with some set theoretic model.</p>
<p>But it definitely &quot;feels&quot; like a &quot;View 2&quot; perspective. I'm not sure how to reconcile this, but there's probably something deep happening.</p>

CC BY-SA 4.0
2021-12-17T21:48:08.370Z
Great summary. Let me add that the *intrinsic view* makes sense mostly as a foundation of mathematics. Computation in general fits the *behavioural view* better, in the sense that at the bottom (whether Turing machines, or actual processors) computation is untyped. Moreover, some forms of computing, in particular parallelism, has not yet come close to anything that could be seen as intrinsically typed.
Martin Berger
CC BY-SA 4.0
2021-12-18T10:29:18.947Z
The answer reminds me of John Reynold's [The meaning of types: From intrinsic to extrinsic semantics](https://kilthub.cmu.edu/articles/journal_contribution/The_Meaning_of_Types_From_Intrinsic_to_Extrinsic_Semantics/6610688). You can find the "domain-theoretic stuff" in there, too.
Andrej Bauer
CC BY-SA 4.0
2022-01-09T19:10:25.687Z
I'm accepting this answer, because I think it very nicely shows that I and Andrej just had different views of what types are; that there are no issues with "set-theoretic" (misnomer or not) quantifiers in my view 2 (which I would perhaps call types-as-invariants) perspective, and that they just (probably) do not make much (or any) sense in the view 1, which I was previously not even aware of. (As a side note, in my magister thesis, I develop a type system that does have these "set-theoretic" quantifiers, although it lacks function types. Will be done in May if everything goes well.)
Jozef Mikušinec
CC BY-SA 4.0
2022-06-22T11:37:18.613Z
My thesis, with "set-theoretic" quantifiers: https://is.muni.cz/th/xr8vu/?lang=en :)
Jozef Mikušinec
CC BY-SA 4.0
2021-12-17T20:40:55.180Z
2021-12-17T20:40:55.180Z
cody
<p>Cody's answer very nicely describes an important distinction. I would just like to point out a specific thing about the interpreation of <span class="math-container">$\forall$</span> as <span class="math-container">$\bigcap$</span>.</p>
<p>A typical way to get <span class="math-container">$\forall$</span> interpreted as an intersection is to use a <a href="https://ncatlab.org/nlab/show/category+of+PERs" rel="nofollow noreferrer">category of PERs</a> on a partial combinatory algebra. Let <span class="math-container">$\mathbb{A}$</span> be an untyped model of computation, such as the untyped <span class="math-container">$\lambda$</span>-calculus, or a universal domain, or Kleene's first partial combinatory algebra. The category <span class="math-container">$\mathsf{PER}(\mathbb{A})$</span> has as its objects partial equivalence relations (symmetric and transitive) on <span class="math-container">$\mathbb{A}$</span>. It is provides a model for all sorts of type systems. In one of them, System F, we interpret <span class="math-container">$\forall$</span> as intersection:
<span class="math-container">$$[\![ \forall X \,.\, \Phi(X) ]\!] = \bigcap_{R \in \mathsf{PER}(\mathbb{A})} [\![\Phi(R)]\!].
$$</span>
One could say that this is a &quot;set-theoretic&quot; interpretation of a quantifier, except that it is not, because we used the category <span class="math-container">$\mathsf{PER}(\mathbb{A})$</span> rather than the category of sets. That is, for something to be called &quot;set-theoretic&quot; it has to use the structure of the category of sets in an essential way. I consider the above use of <span class="math-container">$\bigcap$</span> to be a coincidence: it just so happens that <span class="math-container">$\bigcap$</span> is the infimum operator in the complete lattice of <span class="math-container">$\mathsf{PER}(\mathbb{A})$</span>. To my mind the nature of the model is <em>order-theoretic</em>, not set-theoretic.</p>
<p>In the comments I asked for an explanation of how the OP imagines the &quot;set-like interpretation&quot; of <span class="math-container">$\forall X \,.\, X \to X$</span> because I do not even understand what a &quot;set-like interpretation of quantifiers&quot; is supposed to mean. If we literally interpret <span class="math-container">$\forall$</span> as a class-sized intersection of sets, then <span class="math-container">$\forall X \,.\, X \to X$</span> is going to be empty, so far as <span class="math-container">$X \to X$</span> receives its usual meaning &quot;the set of functional relations from <span class="math-container">$X$</span> to <span class="math-container">$X$</span>&quot;. I still maintain that the problem with this question is not that people (and me in particular) are somehow &quot;against&quot; the set-theoretic interpretation – but that it's not clear at all what that would be, beyond what John Reynolds already wrote about it.</p>

CC BY-SA 4.0
2021-12-18T10:46:16.553Z
2021-12-18T10:46:16.553Z
Andrej Bauer
<p>In <a href="https://cstheory.stackexchange.com/a/32518/48790">his answer</a> to a <a href="https://cstheory.stackexchange.com/questions/32515/universal-and-existential-types">question</a> that tries to treat universal and existential quantifiers as intersections and unions of sets, <a href="https://cstheory.stackexchange.com/users/705/andrej-bauer">Andrej Bauer</a> says:</p>
<blockquote>
<p>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).</p>
</blockquote>
<p>and then introduces the traditional type-theoretic view of universal types as (collections of certain) functions and existential types as (collections of certain) pairs.</p>
<p><strong>Question</strong>: what is wrong with the set-theoretic view? (Why was <a href="https://cstheory.stackexchange.com/users/35510/socumbersome">socumbersome</a> asked to forget it?)</p>
<p><strong>Further details</strong>: 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):</p>
<p><span class="math-container">$$\forall x.T \overset{def}{:=} \bigcap_{S - type} T[x := S] $$</span>
<span class="math-container">$$\exists x.T \overset{def}{:=} \bigcup_{S - type} T[x := S] $$</span></p>
<p>seems to me to be a natural extension of that view.</p>
<p>One (former?) issue I am aware of is that of dealing with cardinality of <span class="math-container">$D$</span> because of <span class="math-container">$D \cong D \to D$</span>. But [0] says: &quot;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]&quot; (the [28] is my [1]).</p>
<p>I even found an old paper[2] that I <em>think</em> (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):</p>
<blockquote>
<p>So say <span class="math-container">$\sigma$</span> is (formally) contractive in t iff one of the
following conditions hold:</p>
<ol>
<li><span class="math-container">$\sigma$</span> has one of the forms bool, int,
<span class="math-container">$t'$</span> (with <span class="math-container">$t' \neq t$</span>),
<span class="math-container">$\sigma_1 \to \sigma_2$</span>, <span class="math-container">$\sigma_1 \times \sigma_2$</span>, or
<span class="math-container">$\sigma_1 + \sigma_2$</span>.</li>
<li><span class="math-container">$\sigma$</span> has one of the forms <span class="math-container">$\sigma_1 \cap \sigma_2$</span>
or <span class="math-container">$\sigma_1 \cup \sigma_2$</span> with
both <span class="math-container">$\sigma_1$</span> and <span class="math-container">$\sigma_2$</span> contractive in t.</li>
<li><span class="math-container">$\sigma$</span> has one of the forms <span class="math-container">$\forall t'.\sigma_1$</span>,
<span class="math-container">$\exists t'.\sigma_1$</span>, or <span class="math-container">$\mu t'.\sigma_1$</span> with either
<span class="math-container">$t' = t$</span> or <span class="math-container">$\sigma_1$</span> contractive in t.</li>
</ol>
<p>Now we take TExp to be the set of well-formed type expressions where <span class="math-container">$\sigma$</span>
is well formed iff one of the following conditions hold:</p>
<ol>
<li><span class="math-container">$\sigma$</span> is bool, int, or t.</li>
<li><span class="math-container">$\sigma$</span> has one of the forms <span class="math-container">$\sigma_1 \to \sigma_2$</span>, <span class="math-container">$\sigma_1 \times \sigma_2$</span>,
<span class="math-container">$\sigma_1 + \sigma_2$</span>, <span class="math-container">$\sigma_1 \cap \sigma_2$</span>, <span class="math-container">$\sigma_1 \cup \sigma_2$</span> with
both <span class="math-container">$\sigma_1$</span> and <span class="math-container">$\sigma_2$</span> well-formed.</li>
<li><span class="math-container">$\sigma$</span> has one of the forms <span class="math-container">$\forall t.\sigma_1$</span> or <span class="math-container">$\exists t.\sigma_1$</span> with <span class="math-container">$\sigma_1$</span> well formed.</li>
<li><span class="math-container">$\sigma$</span> has the form <span class="math-container">$\mu t.\sigma_1$</span> with <span class="math-container">$\sigma_1$</span> well formed
and contractive in t.</li>
</ol>
</blockquote>
<p>Below that it defines an interpretation function
<span class="math-container">$\mathcal{T}\colon \mbox{TExp} \to \mbox{TEnv} \to \mathcal{P}(V)$</span>,
where <span class="math-container">$V$</span> is the space of all values (like booleans, naturals, functions
of those, etc.) with the right isomorphisms.</p>
<p>This paper makes it harder for me to believe there is something
wrong with the &quot;set-theoretic&quot; quantifiers, but maybe I just misunderstand
something important.</p>
<ol start="0">
<li>Advanced Logical Type Systems for Untyped Languages - Andrew M. Kent; <a href="https://pnwamk.github.io/docs/dissertation.pdf" rel="noreferrer">link</a></li>
<li>Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types - Alain Frisch, Giuseppe Castagna, Véronique Benzaken; <a href="https://dl.acm.org/doi/10.1145/1391289.1391293" rel="noreferrer">link</a></li>
<li>An ideal model for recursive polymorphic types - David MacQueen, Gordon Plotkin, Ravi Sethi; <a href="https://www.sciencedirect.com/science/article/pii/S0019995886800195" rel="noreferrer">link</a></li>
</ol>

CC BY-SA 4.0
2021-12-05T11:06:57.923Z
In case you are not already familiar with them, you might be
interested in Pitts', *Polymorphism is set-theoretic, constructively*
which complements Reynolds' *Polymorphism is not Set-Theoretic*.
Martin Berger
CC BY-SA 4.0
2021-12-10T20:50:47.683Z
I am not entirely sure whay you're asking, but does [cody's answer](https://cs.stackexchange.com/a/51731/1329) also answer your question? If not, it would greatly help me to understand what you are asking if you include in your question an explanation of *precisely* how you intend to interpret $\forall X \,.\, (X \to X)$ using intersection, as that will reveal what you have in mind.
Andrej Bauer
CC BY-SA 4.0
2021-12-19T12:05:09.460Z
0/2 @AndrejBauer I have two possible interpretations of quantifiers that I view as "set-theoretic",
in one the quantified variable ranges over values of the programming language,
in the other it ranges over types (or "sets" of values). (The former can be viewed
as the latter where the domain of the quantified variables is restricted to unit
types, (assuming a type system expressive enough to have a unit type for every value).)
Jozef Mikušinec
CC BY-SA 4.0
2021-12-19T12:05:16.310Z
1/2 For me seeing $\forall x.B$ as $\bigcap_xB$ boils down to that any type
$B[x\leftarrow whatever]$ is its supertype, and furthermore $\forall x.B$
is (at least in some sense) the maximal type with this property. So I have two possible
interpretations of $\forall X.X \to X$: the type of the identity function,
or the empty type.

Perhaps you are right that I should call this an order-theoretic, not set-theoretic
view. Thank you to both of you for your answers. I'll wait a few days to see whether
what I wrote changes anything, and then I'll have to decide which one to accept :D
Jozef Mikušinec
CC BY-SA 4.0
2021-12-19T16:10:39.163Z
**Set-theoretically,** a function $f : A \to A$ is a subset $f \subseteq A \times A$ satisfying $\forall x \in A \,.\, \exists! y \in A \,.\, (x, y) \in f$. So, if $A$ and $B$ are disjoint and inhabited, then $(A \to A) \cap (B \to B) = \emptyset$. How are you going to arrange things so that $\forall X . X \to X$ is not empty, or for that matter almost any type of the form $\forall X \,.\, \Phi(x)$? If you are using the symbol $\bigcap$ for something other than intersection, then I don't understand the question (and you should be using a different symbol).
Andrej Bauer
CC BY-SA 4.0
2021-12-19T16:12:28.587Z
Also, if $\forall X . X \to X$ is empty, then you should explain how that relates to programming languages, as one would presumably expect the identity map to inhabit $\forall X . X \to X$.
Andrej Bauer
CC BY-SA 4.0
2021-12-19T16:53:24.080Z
There is another (notational) difference between what I mean by $A \to B$ and the set-theoretic convention that I failed to mention, sorry. I view $A \to B$ as the type of functions whose domain includes $A$ (but may be larger), and such that if $a\colon A$, then $f(a)\colon B$. So the identity function has types $\mathrm{Int} \to \mathrm{Int}$ as well as $\mathrm{Bool} \to \mathrm{Bool}$, as in cody's answer, even though $\mathrm{Int}$ and $\mathrm{Bool}$ are disjoint.
Jozef Mikušinec
CC BY-SA 4.0
2021-12-19T17:02:37.327Z
Regarding functions themselves, those need not be understood set-theoretically as sets of pairs (with unique value per argument). They just need to interact with subtyping in such a way that the subtyping relation looks as if they were. The section 2.5 of "A Gentle Introduction to Semantic Subtyping ([link](https://www.irif.fr/~gc/papers/icalp-ppdp05.pdf))" explains this part better than I can.
Jozef Mikušinec
CC BY-SA 4.0
2021-12-19T17:12:47.010Z
Edit: I just realized that my previous claim that $\forall X.X \to X$ could be the empty type is wrong. Even if $X$ ranges over all types including the empty type $E$, $E \to E$ is the type of all functions, since all values $v\colon E$ vacuously satisfy $f(v)\colon E$. (Previously I made the mistake of thinking that $E \to E$ is empty). So $\forall X.X \to X$ is the type of exactly the identity function.
Jozef Mikušinec
<type-theory><type-systems><set-theory>
What are the issues with a set-like interpretation of quantifiers in type theory?
Jozef Mikušinec
# What are the issues with a set-like interpretation of quantifiers in type theory?

(Asked by: username_0 on 2021-12-04)

In [his answer](https://cstheory.stackexchange.com/a/32518/48790) to a [question](https://cstheory.stackexchange.com/questions/32515/universal-and-existential-types) that tries to treat universal and existential quantifiers as intersections and unions of sets, [username_2](https://cstheory.stackexchange.com/users/705/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](https://cstheory.stackexchange.com/users/35510/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](https://pnwamk.github.io/docs/dissertation.pdf)
1. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types - Alain Frisch, Giuseppe Castagna, Véronique Benzaken; [link](https://dl.acm.org/doi/10.1145/1391289.1391293)
2. An ideal model for recursive polymorphic types - David MacQueen, Gordon Plotkin, Ravi Sethi; [link](https://www.sciencedirect.com/science/article/pii/S0019995886800195)

**Tags:** type-theory, type-systems, set-theory

> **Comments:**
> **username_1**: In case you are not already familiar with them, you might be interested in Pitts', *Polymorphism is set-theoretic, constructively* which complements Reynolds' *Polymorphism is not Set-Theoretic*.  
> **username_2**: I am not entirely sure whay you're asking, but does [username_3's answer](https://cs.stackexchange.com/a/51731/1329) also answer your question? If not, it would greatly help me to understand what you are asking if you include in your question an explanation of *precisely* how you intend to interpret $\forall X \,.\, (X \to X)$ using intersection, as that will reveal what you have in mind.  
> **username_0**: 0/2 @AndrejBauer I have two possible interpretations of quantifiers that I view as "set-theoretic", in one the quantified variable ranges over values of the programming language, in the other it ranges over types (or "sets" of values). (The former can be viewed as the latter where the domain of the quantified variables is restricted to unit types, (assuming a type system expressive enough to have a unit type for every value).)  
> **username_0**: 1/2 For me seeing $\forall x.B$ as $\bigcap_xB$ boils down to that any type $B[x\leftarrow whatever]$ is its supertype, and furthermore $\forall x.B$ is (at least in some sense) the maximal type with this property. So I have two possible interpretations of $\forall X.X \to X$: the type of the identity function, or the empty type.  Perhaps you are right that I should call this an order-theoretic, not set-theoretic view. Thank you to both of you for your answers. I'll wait a few days to see whether what I wrote changes anything, and then I'll have to decide which one to accept :D  
> **username_2**: **Set-theoretically,** a function $f : A \to A$ is a subset $f \subseteq A \times A$ satisfying $\forall x \in A \,.\, \exists! y \in A \,.\, (x, y) \in f$. So, if $A$ and $B$ are disjoint and inhabited, then $(A \to A) \cap (B \to B) = \emptyset$. How are you going to arrange things so that $\forall X . X \to X$ is not empty, or for that matter almost any type of the form $\forall X \,.\, \Phi(x)$? If you are using the symbol $\bigcap$ for something other than intersection, then I don't understand the question (and you should be using a different symbol).  
> **username_2**: Also, if $\forall X . X \to X$ is empty, then you should explain how that relates to programming languages, as one would presumably expect the identity map to inhabit $\forall X . X \to X$.  
> **username_0**: There is another (notational) difference between what I mean by $A \to B$ and the set-theoretic convention that I failed to mention, sorry. I view $A \to B$ as the type of functions whose domain includes $A$ (but may be larger), and such that if $a\colon A$, then $f(a)\colon B$. So the identity function has types $\mathrm{Int} \to \mathrm{Int}$ as well as $\mathrm{Bool} \to \mathrm{Bool}$, as in username_3's answer, even though $\mathrm{Int}$ and $\mathrm{Bool}$ are disjoint.  
> **username_0**: Regarding functions themselves, those need not be understood set-theoretically as sets of pairs (with unique value per argument). They just need to interact with subtyping in such a way that the subtyping relation looks as if they were. The section 2.5 of "A Gentle Introduction to Semantic Subtyping ([link](https://www.irif.fr/~gc/papers/icalp-ppdp05.pdf))" explains this part better than I can.  
> **username_0**: Edit: I just realized that my previous claim that $\forall X.X \to X$ could be the empty type is wrong. Even if $X$ ranges over all types including the empty type $E$, $E \to E$ is the type of all functions, since all values $v\colon E$ vacuously satisfy $f(v)\colon E$. (Previously I made the mistake of thinking that $E \to E$ is empty). So $\forall X.X \to X$ is the type of exactly the identity function.  

---

## 2 answers

### Answer by username_3 on 2021-12-17. Score: 9 | Accepted answer

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.

> **Comments:**
> **username_1**: Great summary. Let me add that the *intrinsic view* makes sense mostly as a foundation of mathematics. Computation in general fits the *behavioural view* better, in the sense that at the bottom (whether Turing machines, or actual processors) computation is untyped. Moreover, some forms of computing, in particular parallelism, has not yet come close to anything that could be seen as intrinsically typed.  
> **username_2**: The answer reminds me of John Reynold's [The meaning of types: From intrinsic to extrinsic semantics](https://kilthub.cmu.edu/articles/journal_contribution/The_Meaning_of_Types_From_Intrinsic_to_Extrinsic_Semantics/6610688). You can find the "domain-theoretic stuff" in there, too.  
> **username_0**: I'm accepting this answer, because I think it very nicely shows that I and Andrej just had different views of what types are; that there are no issues with "set-theoretic" (misnomer or not) quantifiers in my view 2 (which I would perhaps call types-as-invariants) perspective, and that they just (probably) do not make much (or any) sense in the view 1, which I was previously not even aware of. (As a side note, in my magister thesis, I develop a type system that does have these "set-theoretic" quantifiers, although it lacks function types. Will be done in May if everything goes well.)  
> **username_0**: My thesis, with "set-theoretic" quantifiers: https://is.muni.cz/th/xr8vu/?lang=en :)  

---

### Answer by username_2 on 2021-12-18. Score: 4

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](https://ncatlab.org/nlab/show/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.


---

