A Brief History of Types


The history of types involves developments in computer science, logic and philosophy. Here are notes about some of these developments, presented in a roughly chronological order.


(384-322 b.c.)

Among Aristotle's important contributions to philosophical logic was the idea of a category, about which he wrote a book.
The mention of Aristotle is really just to show that if you look hard enough you will find antecedents for the notion of Type way back in the history of ideas.
Formal Logic
Aristotle (384-322 b.c.)set the stage in which our story about types begins. Though he devised his syllogistic logic way back, it remained received wisdom right up to the nineteenth century when Frege found it necessary to throw it out in his search for a formal logic adequate for the derivation of mathematics.

Aristotle also wrote about categories. though these did not play any role in his formal logic they represent for natural languages and metaphysical thought a precedent for the type theoretic idea that semantic considerations limit the kinds of object to which a particular predicate can be appled.


Gottlob Frege, devising a new logic for mathematics, imported functions and functional abstraction into logic from mathematics. The contradictions which arose were the stimulus for the development of logical type theories.
Frege's Foundations
Frege's logical foundations can be observed at two stages, in his Begriffsschrift and his later





UP HOME © RBJ created 1999/9/22 modified 1999/9/22