TAPL Chapter 1: Introduction

A type system is a tractable syntactic method for proving the absense of certain program behaviours by classifying phrases according to the kinds of values they compute

Types systems were first formalised in the 1900’s as a way of avoiding logical paradoxes in mathematics.

Sidenote: Bertrand Russels paradox is to do with the definition of naive set theory. Naive set theory states that any definable collection is a set. the Contradiction arises when you define the set R to be the set of all sets that are not members of themselves. If R is not a member of itself, then it must contain itself, by definition, and if it contains itself, then it doesn’t match its own definition

R = { x | x ∉ x }, then R ∈ R ⟺ R ∉ R