Types of Functional Languages: Coq and Haskell (Part 2/3)

March 2, 2017
coq, haskell, types, dependent types, nondependent types, inductive types, adts
Note: This blog post is a work in progress, check back in a couple days
In part 2 of this series we will investigate the underlying reasons for why Coq and Haskell types are so different. These reasons arise from Coq’s design as a interactive theorem prover Please refer to my previous post for part 1.
The Introduction of Russel’s Paradox
Coq and Haskell are both based on mathematical concepts like set and type theory, both of which came about due to Russell’s Paradox, or the RussellZermelo Paradox. Naïve set theory assumes the socalled naïve or unrestricted Comprehension Axiom. According to naïve set theory, any definable collection is a set. Let R be the set of all sets that are not members of themselves. If R is not a member of itself, then its definition dictates that it must contain itself, and if it contains itself, then it contradicts its own definition as the set of all sets that are not members of themselves. This contradiction is Russell’s paradox.
Let R = {x ∣ x ∉ x}, then R ∈ R ⟺ R ∉ R
Because of this paradox, using classical logic, all sentences follow from a contradiction. For example, assuming both P and ~P, any arbitrary proposition, Q, can be proved as follows: from P we obtain P ∨ Q by the rule of Addition; then from P ∨ Q and ~P we obtain Q by the rule of Disjunctive Syllogism. Because set theory underlies all branches of mathematics, the inconsistency of set theory could mean that no mathematical proof could be completely trustworthy.
In order to bypass this inconsistency, Coq requires sets to exist in universes or ramified types.
CurryHoward Correspondence
The CurryHoward Correspondence, or, “programs as proofs”, relates logic to mathematics, a fundamental discovery that allows to us to create formally verifiable software.
Basic Terms and Types: Inductive Types
 Type theory systems require basic terms and types to operate on
 Functions using Church encoding and inductive types are two examples
 Inductive types are a set of base types and a set of type constructors that generate types with wellbehaved properties
 Certain recursive functions called on inductive types are guaranteed to terminate