GoKawiil< >
Types
In this chapter we will talk about types. This might be disappointing for you, if you expected to learn about as many new categories as possible (which you don’t even suspect are really categories till the unexpected reveal)—we’ve been talking about the category of types in a given programming language ever since the first chapter, and we already know how they form a category. However, types are not just about programming languages. And they are more than just another category. They are also at the heart of a mathematical theory known as type theory.
Type theory is an alternative to set theory, as well as category theory itself, as a foundational language of mathematics, and it is as powerful a tool as any of those formalisms.
Sets, Types and Russell’s paradox
We started talking about sets again. Most books about category theory (and mathematics in general) begin with sets, and often go back to sets. Even in a book about category theory, like this one, the standard definitions of most mathematical objects involve sets. Indeed, upon hearing the definition about monoids being one-object categories, a person who only knows about sets might say:
“Forget that! Have you seen a set? It’s the same thing, but you also have this binary operation.”
Or for orders as being categories with one morphism:
“Have you seen a set? It’s the same thing, but some elements are bigger than others.”
The reason for the prevalence of this “set-centric” viewpoint is actually trivial: sets are simple to understand, especially when we are operating on the conceptual level that is customary for introductory materials.
... continue reading