5 ms·
"If you think of a type as a set of possible values" You can't do that! You fall foul of Russell's paradox - sets as types simply don't work!
by pat_punnu 13y ago
"If you think of a type as a set of possible values"
You can't do that! You fall foul of Russell's paradox - sets as types simply don't work!
- deleted 13y ago[deleted]
- vanderZwan 13y agoElaborate please?
- StefanKarpinski 13y agoAs a consequence/means of avoiding Russel's paradox, the standard axiomatization of set theory (ZFC), doesn't allow sets to contain themselves (so no set of all sets). Thus, if types are sets of values, and types are values, you've got a problem since the type of types seems to be a set that contains itself. Of course, I think this just means that well-founded set theories like ZFC are a poor choice for modeling type systems for languages with first-class types. There are set theories that allow sets to contain themselves [http://en.wikipedia.org/wiki/Non-well-founded_set_theory http://en.wikipedia.org/wiki/Non-well-founded_set_theory]. Such set theories don't replace ZFC, but rather extend it, adding "hypersets", which are the sets that contain themselves – the well-founded sets behave as usual.
- Tobu 13y agoNope, Russel's paradox requires set membership axioms + a non-constructive definition of sets. Types are constructive here.