Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

"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!



Nope, Russel's paradox requires set membership axioms + a non-constructive definition of sets. Types are constructive here.


Elaborate please?


As 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]. 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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: