Type Theory
Feb. 26th, 2003 03:59 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslToday, in a couple of hours I started understanding what type theory is all about, by reading Robert Constable's article / booklet "Naïve Computational Type Theory". I tried to do this from a textbook (Pierce - Types and Programming Languages) for almost a year, but I never made as much progress as I did today.
It seems to be some sort of axiomatically frugal set theory. In some ways, it actually seems more natural than set theory, namely the list (ordered list) object is more primary than set (unordered list) object.
More restrictive logics like Type Theory seem to address a lot of the problems I have with set theory, namely paradoxes about intension (i.e. Russell's), induction, infinity, that whole debate about the axiom of choice, etc. but I am speaking as an outsider, so I ask you experts out there to enlighten me on my confusions.
Would mathematics be any different today if the standard foundation had been type theory instead of set theory?
It seems to be some sort of axiomatically frugal set theory. In some ways, it actually seems more natural than set theory, namely the list (ordered list) object is more primary than set (unordered list) object.
More restrictive logics like Type Theory seem to address a lot of the problems I have with set theory, namely paradoxes about intension (i.e. Russell's), induction, infinity, that whole debate about the axiom of choice, etc. but I am speaking as an outsider, so I ask you experts out there to enlighten me on my confusions.
Would mathematics be any different today if the standard foundation had been type theory instead of set theory?