<p><a href="https://www.irif.fr/%7Egc/slides/icalp-ppdp05-slides.pdf" rel="nofollow noreferrer">Semantic subtyping</a> is based on an underlying set theoretic interpretation of types, where subtyping is subset.  The original <a href="http://www.cduce.org/papers/lics02.ps.gz" rel="nofollow noreferrer">work</a>, I believe, is by Castagna in the context of XML processing language CDuce. Types correspond to sets of XML documents. The ideas have since been <a href="http://www.cduce.org/papers/semantic_pi.pdf" rel="nofollow noreferrer">reapplied</a> to the <span class="math-container">$\pi$</span>-calculus and to a <a href="http://www.lacl.fr/%7Edvaracca/papers/semjava.pdf" rel="nofollow noreferrer">calculus objects and classes</a>.</p>

CC BY-SA 3.0
2012-01-16T07:24:52.370Z
There are precursors to Castagna. A long time ago people already used the subset relation for modeling subtyping in PER models. There a type corresponds to a partial equivalence relation (PER) and subtyping is just inclusion of such relations.
Andrej Bauer
CC BY-SA 4.0
2012-01-15T15:40:16.190Z
2023-03-24T18:55:35.593Z
2023-03-24T18:55:35.593Z
Dave Clarke
<p>With a few exceptions (one which Dave Clarke cites), simple set-theoretic semantics of types are hard to use. The reason is that data abstraction does not play very nicely with set-theoretic semantics. </p>

<p>The basic problem is most easily seen in a total purely functional language with polymorphic types, and consider the polymorphic type $\forall \alpha.\; \alpha \to \alpha$. In a naive set-theoretic semantics of types, we would interpret the function space as set-theoretic function space, and then interpret the universal quantifier as a product over some (small) universe of sets $U$. That is, </p>

<p>$$[\![\forall \alpha.\; \alpha \to \alpha]\!] = \Pi X \in \mathrm{U}.\;X \to X$$</p>

<p>However, note that this interpretation of types includes functions that do something different at each element of $U$ -- we can branch on $U$ to give a different function in $X \to X$ for each $X \in U$. In contrast, the polymorphic type contains <em>only</em> the identity function, since the only operations the programming language will let you perform at type $\alpha$ the ones which work at all types. </p>

<p>So this semantics cannot (for example) justify any optimization based on the fact that the identity is the only inhabitant of $\forall \alpha.\; \alpha \to \alpha$.</p>

CC BY-SA 3.0
2012-01-15T20:43:12.187Z
Neel, I don't think this answer makes sense.  If the semantics of the language are the standard F-style semantics, then a compiler could do the optimization just fine, based on the type system.  If the semantics are the set-theoretic semantics, then the optimization would be unsound.  What model you use for the types doesn't enter into it.
Sam Tobin-Hochstadt
CC BY-SA 3.0
2012-01-16T05:29:40.373Z
Sam, I don't understand your point: it reads like you agree completely with me! The standard set-theoretic semantics cannot prove that the only inhabitant of that type is the identity, so you need a different semantics.
Neel Krishnaswami
CC BY-SA 3.0
2012-01-16T07:27:43.283Z
@Neel: the problem you describe persists even when we move away from sets. The solution is not to change the category of sets with something else, but to model parametricity differently. Namely, one has to use *relational* parametricity, as I am sure you know. But then things work out in sets just as well, if I am not mistaken. The "only" problem with sets is lack of fixed points (both at the level of recursive values and recursive types).
Andrej Bauer
CC BY-SA 3.0
2012-01-16T07:59:29.880Z
Ah, I think I understand why I am confusing you and Sam! I certainly don't mean to imply that it is unsound to use a naive set-theoretic model, just that this model often gives unhelpful answers -- that's why I said "hard to use", and not "wrong". You can of course use sets to build a useful model (i.e., relationally), but then we are no longer intepreting types-as-sets in the fashion suggested in the question. (Also, as you know, with impredicative polymorphism there is no naive model, but parametricity is still meaningful  predicatively.)
Neel Krishnaswami
CC BY-SA 3.0
2012-01-17T23:29:24.680Z
I think your point is about the correspondence between semantics -- a set-theoretic semantics isn't a good fit for System F-style polymorphism, because it has inexpressible inhabitants.  But that's not a point *against* set-theoretic semantics, just a statement that our semantics should agree.  If our language lets us express the functions you're talking about (as Typed Racket does, for example), then we may *want* the set-theoretic semantics.
Sam Tobin-Hochstadt
CC BY-SA 3.0
2012-01-15T16:25:22.637Z
2017-02-13T20:48:31.287Z
2017-02-13T20:48:31.287Z
Neel Krishnaswami
<p>The main reason for avoiding sets in semantics of types is that a typical programming language allows us to define arbitrary recursive functions. Therefore, whatever the meaning of a type is, it has to have the fixed-point property. The only set with such a property is the singleton set.</p>
<p>To be more precise, a recursively defined value <span class="math-container">$v$</span> of type <span class="math-container">$\tau$</span> (where typically <span class="math-container">$\tau$</span> is a function type) is defined by a fixed-point equation <span class="math-container">$v = \Phi(v)$</span> where <span class="math-container">$\Phi : \tau \to \tau$</span> can be any program. If <span class="math-container">$\tau$</span> is interpreted as the set <span class="math-container">$T$</span> then we would expect every <span class="math-container">$f : T \to T$</span> to have a fixed point. But the only set <span class="math-container">$T$</span> with this property is the singleton.</p>
<p>Of course, you could also realize that the culprit is classical logic. If you work with intuitionistic set theory, then it is consistent to assume that there are many sets with fixed-point property. In fact, this has been used to give semantics of programming language, see for example</p>
<blockquote>
<p>Alex Simpson, <em><a href="https://web.archive.org/web/20130425174944/https://homepages.inf.ed.ac.uk/als/Research/cartinmist.pdf" rel="nofollow noreferrer">Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory</a></em>, In Annals of Pure and Applied Logic, 130:207-275, 2004.</p>
</blockquote>

CC BY-SA 4.0
2012-01-15T19:49:05.317Z
2023-03-24T18:55:23.953Z
2023-03-24T18:55:23.953Z
Andrej Bauer
<p>As I understand, in computer science data types are not based on set theory because of things like Russell's paradox, but as in real world programming languages we can't express such complex data types as "set that does not contain itself", can we say that in practice type is an infinite set of its members where instance membership is defined by of number of features that are intrinsic to this type/set (existence of certain properties, methods)? If no what would be the counterexample?</p>

CC BY-SA 3.0
2012-01-15T22:03:17.287Z
Russell's paradox has nothing to do with it directly.
Andrej Bauer
<type-theory><set-theory><type-systems>
Type system based on naive set theory
Nutel
# Type system based on naive set theory

(Asked by: username_0 on 2012-01-15)

As I understand, in computer science data types are not based on set theory because of things like Russell's paradox, but as in real world programming languages we can't express such complex data types as "set that does not contain itself", can we say that in practice type is an infinite set of its members where instance membership is defined by of number of features that are intrinsic to this type/set (existence of certain properties, methods)? If no what would be the counterexample?

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

> **Comments:**
> **username_1**: Russell's paradox has nothing to do with it directly.  

---

## 3 answers

### Answer by username_1 on 2012-01-15. Score: 15 | Accepted answer

The main reason for avoiding sets in semantics of types is that a typical programming language allows us to define arbitrary recursive functions. Therefore, whatever the meaning of a type is, it has to have the fixed-point property. The only set with such a property is the singleton set.

To be more precise, a recursively defined value $v$ of type $\tau$ (where typically $\tau$ is a function type) is defined by a fixed-point equation $v = \Phi(v)$ where $\Phi : \tau \to \tau$ can be any program. If $\tau$ is interpreted as the set $T$ then we would expect every $f : T \to T$ to have a fixed point. But the only set $T$ with this property is the singleton.

Of course, you could also realize that the culprit is classical logic. If you work with intuitionistic set theory, then it is consistent to assume that there are many sets with fixed-point property. In fact, this has been used to give semantics of programming language, see for example

> Alex Simpson, *[Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory](https://web.archive.org/web/20130425174944/https://homepages.inf.ed.ac.uk/als/Research/cartinmist.pdf)*, In Annals of Pure and Applied Logic, 130:207-275, 2004.


---

### Answer by username_2 on 2012-01-15. Score: 8

[Semantic subtyping](https://www.irif.fr/%7Egc/slides/icalp-ppdp05-slides.pdf) is based on an underlying set theoretic interpretation of types, where subtyping is subset. The original [work](http://www.cduce.org/papers/lics02.ps.gz), I believe, is by Castagna in the context of XML processing language CDuce. Types correspond to sets of XML documents. The ideas have since been [reapplied](http://www.cduce.org/papers/semantic_pi.pdf) to the $\pi$-calculus and to a [calculus objects and classes](http://www.lacl.fr/%7Edvaracca/papers/semjava.pdf).

> **Comments:**
> **username_1**: There are precursors to Castagna. A long time ago people already used the subset relation for modeling subtyping in PER models. There a type corresponds to a partial equivalence relation (PER) and subtyping is just inclusion of such relations.  

---

### Answer by username_3 on 2012-01-15. Score: 6

With a few exceptions (one which username_2 cites), simple set-theoretic semantics of types are hard to use. The reason is that data abstraction does not play very nicely with set-theoretic semantics.

The basic problem is most easily seen in a total purely functional language with polymorphic types, and consider the polymorphic type $\forall \alpha.\; \alpha \to \alpha$. In a naive set-theoretic semantics of types, we would interpret the function space as set-theoretic function space, and then interpret the universal quantifier as a product over some (small) universe of sets $U$. That is,

$$[\![\forall \alpha.\; \alpha \to \alpha]\!] = \Pi X \in \mathrm{U}.\;X \to X$$

However, note that this interpretation of types includes functions that do something different at each element of $U$ -- we can branch on $U$ to give a different function in $X \to X$ for each $X \in U$. In contrast, the polymorphic type contains *only* the identity function, since the only operations the programming language will let you perform at type $\alpha$ the ones which work at all types.

So this semantics cannot (for example) justify any optimization based on the fact that the identity is the only inhabitant of $\forall \alpha.\; \alpha \to \alpha$.

> **Comments:**
> **username_4**: Neel, I don't think this answer makes sense.  If the semantics of the language are the standard F-style semantics, then a compiler could do the optimization just fine, based on the type system.  If the semantics are the set-theoretic semantics, then the optimization would be unsound.  What model you use for the types doesn't enter into it.  
> **username_3**: Sam, I don't understand your point: it reads like you agree completely with me! The standard set-theoretic semantics cannot prove that the only inhabitant of that type is the identity, so you need a different semantics.  
> **username_1**: @Neel: the problem you describe persists even when we move away from sets. The solution is not to change the category of sets with something else, but to model parametricity differently. Namely, one has to use *relational* parametricity, as I am sure you know. But then things work out in sets just as well, if I am not mistaken. The "only" problem with sets is lack of fixed points (both at the level of recursive values and recursive types).  
> **username_3**: Ah, I think I understand why I am confusing you and Sam! I certainly don't mean to imply that it is unsound to use a naive set-theoretic model, just that this model often gives unhelpful answers -- that's why I said "hard to use", and not "wrong". You can of course use sets to build a useful model (i.e., relationally), but then we are no longer intepreting types-as-sets in the fashion suggested in the question. (Also, as you know, with impredicative polymorphism there is no naive model, but parametricity is still meaningful  predicatively.)  
> **username_4**: I think your point is about the correspondence between semantics -- a set-theoretic semantics isn't a good fit for System F-style polymorphism, because it has inexpressible inhabitants.  But that's not a point *against* set-theoretic semantics, just a statement that our semantics should agree.  If our language lets us express the functions you're talking about (as Typed Racket does, for example), then we may *want* the set-theoretic semantics.  

---

