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

It's a common misconception that Russell/Whitehead "invented" type theory. In fact, Frege had already made the very insightful distinction between functional and non-functional types in the 1890s -- this was the key development that Russell based his hierarchy of types on. See "Function and Concept" (1891)[1]. It was a growing and communal sentiment that a (meta-)theory of types would make certain mathematical concepts more palatable.

If anything, I think the conceptual father of type theory is Gottlob Frege, and Alonzo Church was the first to apply it concretely.

[1] http://fitelson.org/proseminar/frege_fac.pdf



It seems to me Frege understood the need in mathematics to talk about many different kinds of thing - numbers, truth-values, functions, and so forth - and to distinguish which kind of thing you are talking about; but not the necessity to use types (or other methods) to avoid circularity. Indeed, it is precisely the mistake Frege made in his attempt to axiomatise logic and mathematics and which led to Russell's paradox, that motivated Russell (and Whitehead)'s theories of types.

Frege certainly articulated a clear notion of what a function is, which is significant.




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

Search: