First, here is a note about the notation that I will use here: Let `1` denote the unit type, the type with one inhabitant. Let `()` denote the inhabitant of the

First, here is a note about the notation that I will use here: Let `1` denote the unit type, the type with one inhabitant. Let `()` denote the inhabitant of the unit type. Let `a + b` or `Either a b` denote the sum of types `a` and `b`. Let `Left` and `Right` be the constructors of the sum type. Before defining the integers, one must define the natural numbers. Natural numbers are defined as an inductive type, which is a little different from an ordinary sum type: data Nat = Z | Suc Nat Here is another way of defining them. Start by removing the self-reference: data NatF a = Z | Suc a Notice that NatF is the same thing as the Maybe/Option type, AKA 1+a, AKA the sum of the unit type and a. Given a "fix" type: data Fix f = MkFix (f (Fix f)) the definition of the natural numbers would be: type Nat = Fix NatF An "F-algebra" is a way of defining some algebraic structure or data type as a map from a "sum of products" to the type. More precisely, an F-algebra consists of an "object" (type) A and a map F(A) -> A. For the natural numbers, the F is NatF and the map would be a function mkNat : NatF Nat -> Nat, AKA mkNat : (Maybe Nat) -> Nat or mkNat : (1 + Nat) -> Nat. Related links: - https://ncatlab.org/nlab/show/inductive+type https://ncatlab.org/nlab/show/inductive+type - https://ncatlab.org/nlab/show/natural+numbers+object https://ncatlab.org/nlab/show/natural+numbers+object - https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunc... - https://en.wikipedia.org/wiki/F-algebra https://en.wikipedia.org/wiki/F-algebra --- One way of defining the integers is as the product of the natural numbers with themselves, or Nat * Nat, equipped with an equivalence relation ~ where (a, b) ~ (c, d) := a + d = b + c (a, b) can be understood as a - b. Of course, a - b = c - d <-> a + d = b + c. Another way of defining the integers is as: data Int = Neg Nat | Zero | Pos Nat where 0 = Zero, -1 = Neg Z, and +1 = Pos Z. --- Booleans can be defined as 1 + 1. Left () = True and Right () = False, or vice versa.