# Type system based on naive set theory

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?

• Russell's paradox has nothing to do with it directly. – Andrej Bauer Jan 15 '12 at 22:03

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, In Annals of Pure and Applied Logic, 130:207-275, 2004.

Semantic subtyping is based on an underlying set theoretic interpretation of types, where subtyping is subset. The original work, 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 to the $\pi$-calculus and to a calculus objects and classes.

• 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 Jan 16 '12 at 7:24

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.

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$.

• 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 Jan 15 '12 at 20:43
• 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 Jan 16 '12 at 5:29
• @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 Jan 16 '12 at 7:27
• 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 Jan 16 '12 at 7:59
• 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 Jan 17 '12 at 23:29