A chapter from 'Category Theory Illustrated' covering type theory as an alternative foundation to set theory. It begins with Russell's paradox and how it motivated both ZFC set theory and Russell's type theory. The chapter explains how types are defined via formation, introduction, and elimination rules, then walks through defining Bool, Maybe, Nat, List, Tuple, and Either types in Haskell using GADTs. It covers Church encoding, Simply-typed Lambda Calculus, Polymorphic Lambda Calculus (System F), and concludes with the Curry-Howard-Lambek correspondence linking intuitionistic logic, lambda calculus, and Cartesian Closed Categories.
Table of contents
Sets, Types and Russell’s paradoxWhat is type theoryBase types. The boolean typePolymorphic types. The Maybe typeInductive types. The natural number type.Composite types. The list type.Positive and negative types. Either and Tuples.Church encoding: From Haskell to Lambda CalculusPolymorphic lambda calculus – Formal definitionType systems as CategoriesCurry-Howard-Lambek correspondenceAppendix: definitions in HaskellAnswersSort: