In a modern age of programming we have become quite acquainted with the idea of mathematical types. Mathematical types proliferate through functional programming languages and have made greater bounds in the guise of modern programming languages. However, types have a longer and richer history than Haskell and Rust. Here I attempt to tackle why these mysterious constructs that seem useful for programming are almost entirely unrelated, and do they have a deeper meaning.

Set Theory as a foundation to Logic

We often view set theory as natural, like something that always existed that way. However in the bigger reality of sets, they weren’t always treated as natural mathematical objects. The question of set theory I have always found to be foundationally epistemic in nature. To us who work with mathematical structures all the time (except those who work with mathematical structures more than I do) sets are fundamental.

The Sigma Type

Consider the following Σ_x : ℕℝ test

x² + y² = h² Σ_{x : ℕ}ℝ

Σ_x : ℕℝ