10
$\begingroup$

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.

  1. Advanced Logical Type Systems for Untyped Languages - Andrew M. Kent; link
  2. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types - Alain Frisch, Giuseppe Castagna, Véronique Benzaken; link
  3. An ideal model for recursive polymorphic types - David MacQueen, Gordon Plotkin, Ravi Sethi; link
$\endgroup$
9
  • 3
    $\begingroup$ 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. $\endgroup$ Dec 5, 2021 at 11:06
  • 1
    $\begingroup$ I am not entirely sure whay you're asking, but does cody's answer 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. $\endgroup$ Dec 10, 2021 at 20:50
  • $\begingroup$ 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).) $\endgroup$ Dec 19, 2021 at 12:05
  • $\begingroup$ 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 $\endgroup$ Dec 19, 2021 at 12:05
  • $\begingroup$ 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). $\endgroup$ Dec 19, 2021 at 16:10

2 Answers 2

8
$\begingroup$

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.

$\endgroup$
4
  • 2
    $\begingroup$ 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. $\endgroup$ Dec 17, 2021 at 21:48
  • 1
    $\begingroup$ The answer reminds me of John Reynold's The meaning of types: From intrinsic to extrinsic semantics. You can find the "domain-theoretic stuff" in there, too. $\endgroup$ Dec 18, 2021 at 10:29
  • 1
    $\begingroup$ 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.) $\endgroup$ Jan 9 at 19:10
  • 1
    $\begingroup$ My thesis, with "set-theoretic" quantifiers: is.muni.cz/th/xr8vu/?lang=en :) $\endgroup$ Jun 22 at 11:37
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.