What are some examples of types that can't be derived set theoretically?

Question

I'm hoping for examples that aren't too abstract or useless in day-to-day programming, though not with a lot of hope, since in Bartosz Milewski's book, it is stated that generally speaking, the category Set is good enough, but mentions polymorphic functions and there not being a set that includes all sets as being one possible example.

For polymorphic functions, I'm not really sure how this comes up. For example, with id[A](x: A): x -> x, where A is a type parameter, I do not see why we could not just say: A is a member of the type universe corresponding to our programming language, which would just be the set of all types supported by our language. Perhaps if our programming language supports a type universe hierarchy, then this argument could be made, but I do not know if any languages do support it in any meaningful way (perhaps theorem proving languages like CoQ?)

Notes on answers

Recursively defined types

For type t = bool + (t -> t), since we assume t corresponds to a set T, t->t would be size T^T (ref). In Scala it looks like this:

sealed trait T
final case class Foo(value: Boolean) extends T
final case class Bar(value: T => T) extends T 

Answer 1

There are several type-theoretic constructions that cannot be easily handled with set theory. Note that when we say "set theory" we mean that we intend to interpret types as sets and type-theoretic functions as set-theoretic functions. In particular, the set-theoretic interpretation of types requires that a function type A → B must be interpreted as the set of all set-theoretic functions from A to B.

If our type theory has general recursion then it cannot be interpreted set-theoretically. General recursion allows us to define, for any type A, the fixed-point operator fix : (A → A) → A

fix f = f (fix f)

but the only sets which have such a fixed-point operator are the singletons. For example, if we take A to have two elements, then it will have a function without fixed point (the one that swaps the elements).

Another reason that set theory may not be sufficient is polymorphism, as you indicated. Here the reasons are perhaps a bit technical and it is best to read the famous paper Polymorphism is not set-theoretic by John Reynolds. Beware: reasoning about how one might get away with a polymorphic identity function is not proof that set theory models polymorphism. In any case, your suggestion to use universes is not going to work for System F. You can have an identity function that works for one universe, but to make it work for all universes you will have to make it universe-polymorphic, and so you're back to square one.

A third reason that a type theory may not be set-theoretic is that it allows constructions of types that do not exist in set theory. For example, in many programming languages we can define recursive types (Haskell and ML are like this) such as

type t = bool + (t -> t)

The set-theoretic counterpart of this is a set T such that $$T \cong 2 + T^T$$ but such a set $T$ does not exist, because the cardinality of $2 + T^T$ is strcictly larger than the cardinality of $T$.

A fourth reason that a type theory may not be set-theoretic is that it may contain constructs that prevent this. For example, we could have a type theory with a timeout construct which works as follows: timeout k x e computes e for at most k steps (where "step" need to be suitably defined). If e finishes with result y within k steps then the overall result is y, otherwise the overall result is the "fallback" value x. From a programming point of view, this is a reasonable construct that can actually be implemented. However, as soon as we have timeout we can write down functions that do not exist in set theory. One such function is the modulus of continuity which witnesses the fact that "all functions are continuous". In set theory there are many discontinuous functions.

Lastly, if we take "spartan" type theory without any special features (no general recursion, no polymorphism, no recursive types, etc.) then it is set theoretic. You need to extend type theory in some fashion to break the set-theoretic interpretation.