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

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 Russell-Zermelo Paradox. Naïve set theory assumes the so-called 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.

Curry-Howard Correspondence

The Curry-Howard 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 well-behaved properties
  • Certain recursive functions called on inductive types are guaranteed to terminate