4
$\begingroup$

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 
$\endgroup$
  • 2
    $\begingroup$ Maybe this has to do with impredicativity? If you have Set:Set in set-theory, you get Russel's paradox, but you get something similar in System F/Calculus of Constructions without contradiction. $\endgroup$ – jmite Mar 5 '18 at 22:11
  • $\begingroup$ @jmite - like recursive types (en.wikipedia.org/wiki/Recursive_data_type)? It seems like even if the definition of List[A] is not set theoretic, there is an equivalent definition that is: the union of {Nil} with the set of all lists whose elements are of typeA. $\endgroup$ – bbarker Mar 5 '18 at 22:43
  • 1
    $\begingroup$ No, impredicativity has to do with whether Type contains itself. If v:T then T:Type, but does Type:Type hold? It does in System F/Calculus of Constructions, but it doesn't for Martin-Lof Type Theory. A side effect of this is that impredicative systems can instantiate polymorphic types with polymorphic parameters, but predicative systems cannot. Agda, Idris, and Set in Coq are predicative, because of the universe restrictions. But Prop in Coq is impredicative. $\endgroup$ – jmite Mar 5 '18 at 23:20
  • $\begingroup$ I should probably get familiar with CoQ, but it sounds as though Scala and Haskell may qualify due to having type systems supporting (variants of) System F. Will try to post an example soon. $\endgroup$ – bbarker Mar 6 '18 at 2:13
  • $\begingroup$ In your example, you let A to rangle only on "the type universe" (whatever that is), unlike all of Set. So, you are not using Set, but something else: what, exactly? After you define that, try to instantiate the identity to its own type (impredicatively), so that $id : (\forall a.a\to a) \to (\forall a.a\to a) $. Does your universe allows that? $\endgroup$ – chi Mar 6 '18 at 14:00
9
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks for the excellent response; I'm slowly going through this. A minor question for now: if you know of a language that can support something like type t = bool + (t -> t), I'd love to play around with it. I tried in Haskell but do not know it well, and it didn't seem easily possible. $\endgroup$ – bbarker Mar 9 '18 at 17:13
  • 1
    $\begingroup$ The type is defined like this in Haskell: data T = Foo Bool | Bar (T -> T) (you have to name each summand, I named them Foo and Bar in time honored tradition). You can then have, for instance Bar (\x -> x). $\endgroup$ – Andrej Bauer Mar 9 '18 at 22:09
  • $\begingroup$ I really enjoyed the type t example; it probably comes up quite frequently in practice (or something similar to it). I'm having trouble understanding how fix f relates to needing something beyond set theory; just because non-singleton sets admit functions without fixed points, doesn't mean we can't model fixed point functions in a set theoretic context, does it? $\endgroup$ – bbarker Mar 15 '18 at 15:25

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.