This post will explain the connection between programming languages and logical proofs, known as the Curry-Howard correspondence. I will provide several examples of this correspondence to help you build a working intuition for how these two fields relate to one another.
The Curry-Howard correspondence states that:
- Logical propositions correspond to programming types
- Logical proofs correspond to programming values
- Proving a proposition corresponds to creating a value of a given type
I'll use my Dhall programming language to illustrate the above connections since Dhall is an explicitly typed total programming language without any escape hatches. If you're not familiar with Dhall, you can read the Dhall tutorial and I will also make analogies to Haskell along the way, too.
Propositions
Let's begin with the following logical proposition:
∀(a ∈ Prop): a ⇒ a
You can read that as "for any proposition (which we will denote using the letter a), if the proposition a is true then the proposition a is true". This is true no matter what the proposition a is. For example, suppose that a were the following proposition:
a = {The sky is blue}
Then we could conclude that "if the sky is blue then the sky is blue":
{The sky is blue} ⇒ {The sky is blue}
Here the right double arrow (⇒) denotes logical implication. Anywhere you see (A ⇒ B) you should read that as "if the proposition A is true then the proposition B is true". You can also say "the proposition A implies the proposition B" or just "A implies B" for short.
However, what if a were another proposition like:
a = {The sky is green}
giving us:
{The sky is green} ⇒ {The sky is green}
This is true, even though the sky might not be green. We only state that "if the sky is green then the sky is green", which is definitely a true statement, whether or not the sky is green.
The upside down A (i.e. ∀) in our original proposition is mathematical shorthand that means "for all" (although I sometimes describe this as "for any"). The ∈ symbol is shorthand for "in" (i.e. set membership). So whenever you see this:
∀(a ∈ S): p
... you can read that as "for any element a in the set S the proposition p is true". Usually the set S is Prop (i.e. the set of all possible propositions) but we will see some examples below where S can be another set.
Types
This logical proposition:
∀(a ∈ Prop): a ⇒ a
... corresponds to the following Dhall type:
... which you can read as "for any type (which we will denote using the letter a), this is the type of a function that transforms an input of type a to an output of type a". Here's the corresponding function that has this type:
λ(a : Type) → λ(x : a) → x
This is an anonymous function of two arguments:
- the first argument is named
a and a is a Type
- the second argument is named
x and x has type a
The result is the function's second argument (i.e. x) which still has type a.
The equivalent Haskell function is id, the polymorphic identity function:
id :: a -> a
id x = x
-- or using the `ExplicitForAll` language extension
id :: forall a . a -> a
id x = x
The main difference is that Haskell does not require you to explicitly bind the polymorphic type a as an additional argument. Dhall does require this because Dhall is an explicitly typed language.
Correspondence
The Curry-Howard correspondence says that we can use the type checker of a programming language as a proof checker. Any time we want to prove a logical proposition, we:
- translate the logical proposition to the corresponding type in our programming language
- create a value in our programming language that has the given type
- use the type-checker to verify that our value has the specified type
If we find a value of the given type then that completes the proof of our original proposition.
For example, if we want to prove this proposition:
∀(a ∈ Prop): a ⇒ a
... then we translate the proposition to the corresponding type in the Dhall programming language:
... then define a value in the Dhall language that has this type:
λ(a : Type) → λ(x : a) → x
... and then use Dhall's type checker to verify that this value has the given type:
$ dhall <<< 'λ(a : Type) → λ(x : a) → x'
∀(a : Type) → ∀(x : a) → a
λ(a : Type) → λ(x : a) → x
The first line is the inferred type of our value and the second line is the value's normal form (which in this case is the same as the original value).
Note that the inferred type slightly differs from the original type we expected:
-- What we expected:
∀(a : Type) → a → a
-- What the compiler inferred:
∀(a : Type) → ∀(x : a) → a
These are both still the same type. The difference is that the compiler's inferred type also includes the name of the second argument: x. If we were to translate this back to logical proposition notation, we might write:
∀(a ∈ Prop): ∀(x ∈ a): a
... which you could read as: "for any proposition named a, given a proof of a named x, the proposition a is true". This is equivalent to our original proposition but now we've given a name (i.e. x) to the proof of a.
The reason this works is that you can think of a proposition as a set, too, where the elements of the set are the proofs of that proposition. Some propositions are false and have no elements (i.e. no valid proofs), while other propositions can have multiple elements (i.e. multiple valid proofs).
Similarly, you can think of a type as a set, where the elements of the set are the values that have that type. Some types are empty and have no elements (i.e. no values of that type), while other types can have multiple elements (i.e. multiple values of that type).
Here's an example of a proposition that has multiple valid proofs:
∀(a ∈ Prop): a ⇒ a ⇒ a
The corresponding type is:
... and there are two values that have the above type. The first value is:
λ(a : Type) → λ(x : a) → λ(y : a) → x
... and the second value is:
λ(a : Type) → λ(x : a) → λ(y : a) → y
We can even translate these two values back into informal logical proofs. For example, this value:
λ(a : Type) → λ(x : a) → λ(y : a) → x
... corresponds to this informal proof:
For each "a" in the set of all propositions:
Given a proof that "a" is true [Let's call this proof "x"]
Given a proof that "a" is true [Let's call this proof "y"]
We can conclude that "a" is true, according to the proof "x"
QED
Similarly, this value:
λ(a : Type) → λ(x : a) → λ(y : a) → y
... corresponds to this informal proof:
For each "a" in the set of all propositions:
Given a proof that "a" is true [Let's call this proof "x"]
Given a proof that "a" is true [Let's call this proof "y"]
We can conclude that "a" is true, according to the proof "y"
QED
We can actually give these proofs a formal structure that parallels our code but that is outside of the scope of this post.
Function composition
Now consider this more complex proposition:
∀(a ∈ Prop):
∀(b ∈ Prop):
∀(c ∈ Prop):
(b ⇒ c) ⇒ (a ⇒ b) ⇒ (a ⇒ c)
You can read that as saying: "for any three propositions named a, b, and c, if b implies c, then if a implies b, then a implies c".
The corresponding type is:
∀(a : Type)
→ ∀(b : Type)
→ ∀(c : Type)
→ (b → c) → (a → b) → (a → c)
... and we can define a value that has this type in order to prove that the proposition is true:
λ(a : Type)
→ λ(b : Type)
→ λ(c : Type)
→ λ(f : b → c)
→ λ(g : a → b)
→ λ(x : a)
→ f (g x)
... and the compiler will infer that our value has the correct type:
$ dhall
λ(a : Type)
→ λ(b : Type)
→ λ(c : Type)
→ λ(f : b → c)
→ λ(g : a → b)
→ λ(x : a)
→ f (g x)
<Ctrl-D>
∀(a : Type) → ∀(b : Type) → ∀(c : Type) → ∀(f : b → c) → ∀(g : a → b) → ∀(x : a) → c
λ(a : Type) → λ(b : Type) → λ(c : Type) → λ(f : b → c) → λ(g : a → b) → λ(x : a) → f (g x)
Note that this function is equivalent to Haskell's function composition operator (ie. (.)):
(.) :: (b -> c) -> (a -> b) -> (a -> c)
(f . g) x = f (g x)
This is because proofs and programs are equivalent to one another: whenever we prove a logical proposition we get a potentially useful function for free.
Circular reasoning
There are some propositions that we cannot prove, like this one:
∀(a ∈ Prop): a
... which you can read as saying "all propositions are true". This proposition is false, because if we translate the proposition to the corresponding type:
... then there is no value in the Dhall language which has that type. If there were such a value then we could automatically create any value of any type.
However, Haskell does have values which inhabit the above type, such as this one:
example :: a
example = let x = x in x
-- or using the `ExplicitForAll` language extension:
example :: forall a . a
example = let x = x in x
This value just cheats and endlessly loops, which satisfies Haskell's type checker but doesn't produce a useful program. Unrestricted recursion like this is the programming equivalent of "circular reasoning" (i.e. trying to claim that a is true because a is true).
We can't cheat like this in Dhall and if we try we just get this error:
$ dhall <<< 'let x = x in x'
Use "dhall --explain" for detailed errors
Error: Unbound variable
x
(stdin):1:9
You cannot define x in terms of itself because Dhall does not permit any recursion and therefore does not permit circular reasoning when used as a proof checker.
And
We will use the symbol ∧ to denote logical "and", so you can read the following proposition:
∀(a ∈ Prop): ∀(b ∈ Prop): (a ∧ b) ⇒ a
... as saying "for any two propositions a and b, if a and b are both true then a is true"
The type-level equivalent of logical "and" is a record with two fields:
∀(a : Type) → ∀(b : Type) → { fst : a, snd : b } → a
... which is equivalent to this Haskell type:
(a, b) -> a
-- or using `ExplicitForAll`:
forall a b . (a, b) -> a
The programming value that has this type is:
λ(a : Type) → λ(b : Type) → λ(r : { fst : a, snd : b }) → r.fst
... which is equivalent to this Haskell value:
Similarly, we can conclude that:
∀(a ∈ Prop): ∀(b ∈ Prop): (a ∧ b) ⇒ b
... which corresponds to this type:
∀(a : Type) → ∀(b : Type) → { fst : a, snd : b } → b
... and this value of that type as the proof:
λ(a : Type) → λ(b : Type) → λ(r : { fst : a, snd : b }) → r.snd
Now let's try a slightly more complex proposition:
∀(a ∈ Prop): ∀(b ∈ Prop): (a ∧ (a ⇒ b)) ⇒ b
You can read this as saying "for any propositions a and b, if the proposition a is true, and a implies b, then the proposition b is true".
That corresponds to this type:
∀(a : Type) → ∀(b : Type) → { fst : a, snd : a → b } → b
... and the following value of that type which proves that the proposition is true:
λ(a : Type)
→ λ(b : Type)
→ λ(r : { fst : a, snd : a → b })
→ r.snd r.fst
Here's a slightly more complex example:
∀(a ∈ Prop): ∀(b ∈ Prop): ∀(c ∈ Prop): ((a ∧ b) ⇒ c) ⇒ (a ⇒ b ⇒ c)
You can read that as saying: "for any three propositions named a, b, and c, if a and b imply c, then a implies that b implies c".
Here's the corresponding type:
∀(a : Type)
→ ∀(b : Type)
→ ∀(c : Type)
→ ({ fst : a, snd : b } → c) → (a → b → c)
... and the corresponding value of that type:
λ(a : Type)
→ λ(b : Type)
→ λ(c : Type)
→ λ(f : { fst : a, snd : b } → c)
→ λ(x : a)
→ λ(y : b)
→ f { fst = x, snd = y }
Note that this is equivalent to Haskell's curry function:
curry :: ((a, b) -> c) -> (a -> b -> c)
curry f x y = f (x, y)
Or
We will use the symbol ∨ to denote logical "or", so you can read the following proposition:
∀(a ∈ Prop): ∀(b ∈ Prop): a ⇒ a ∨ b
... as saying "for any propositions a and b, if a is true, then either a is true or b is true".
The type-level equivalent of logical "or" is a sum type:
∀(a : Type) → ∀(b : Type) → a → < Left : a | Right : b >
... which is equivalent to this Haskell type:
a -> Either a b
-- or using `ExplicitForAll`
forall a b . a -> Either a b
... and the value that has this type is:
λ(a : Type) → λ(b : Type) → λ(x : a) → < Left = x | Right : b >
... which is equivalent to this Haskell value:
Similarly, for this proposition:
∀(a ∈ Prop): ∀(b ∈ Prop): b ⇒ a ∨ b
... the equivalent type is:
∀(a : Type) → ∀(b : Type) → b → < Left : a | Right : b >
... and the value that has this type is:
λ(a : Type) → λ(b : Type) → λ(x : b) → < Right = x | Left : a >
Let's consider a more complex example:
∀(a ∈ Prop): a ∨ a ⇒ a
... which says: "for any proposition a, if a is true or a is true then a is true".
The corresponding type is:
∀(a : Type) → < Left : a | Right : a > → a
... which is equivalent to this Haskell type:
Either a a -> a
-- or using `ExplicitForAll`
forall a . Either a a -> a
... and we can create a value of this type by pattern matching on the sum type:
λ(a : Type)
→ λ(s : < Left : a | Right : a >)
→ merge
{ Left = λ(x : a) → x
, Right = λ(x : a) → x
}
s
: a
... which is equivalent to this Haskell code:
example :: Either a a -> a
example (Left x) = x
example (Right x) = x
You can read this "proof" as saying: "There are two possibilities. The first possibility (named "Left") is that a is true, therefore a must be true in that case. The second possibility (named "Right") is that a is true, therefore a must be true in that case. Since a is true in both cases we can conclude that a is true, period."
True
We'll use True to denote a logical proposition that is always true:
True
... and the corresponding type is an empty record with no fields:
... which is equivalent to Haskell's "unit" type:
An empty record literal is the only value that has the type of an empty record:
... which is equivalent to Haskell's "unit" value:
False
We'll use False to denote a logical proposition that is never true:
False
... and the corresponding type is an empty sum type (i.e. a type with no constructors/alternatives):
... which is equivalent to Haskell's Void type.
There is no value that has the above type, so you cannot prove a False proposition.
The logical "principle of explosion" states that if you assume a False proposition then you can prove any other proposition. In other words:
False ⇒ ∀(a ∈ Prop): a
... which you can read as saying: "if you assume a false proposition, then for any proposition named a you can prove that a is true".
The corresponding type is:
... and the value that inhabits the above type is:
λ(s : <>) → λ(a : Type) → merge {=} s : a
You can read that "proof" as saying: "There are zero possibilities. Since we handled all possibilities then the proposition a must be true." This line of reasoning is called a "vacuous truth", meaning that if there are no cases to consider then any statement you make is technically true for all cases.
The equivalent Haskell type would be:
... and the equivalent Haskell value of that type would be:
Not
We'll use not to negate a logical proposition, meaning that:
not(True) = False
not(False) = True
We can encode logical not in terms of logical implication and logical False, like this:
not(a) = a ⇒ False
not(True) = True ⇒ False = False
not(False) = False ⇒ False = True
If logical not is a function from a proposition to another proposition then type-level not must be a function from a type to a type:
We can save the above type-level function to a file to create a convenient ./not utility we will reuse later on:
$ echo 'λ(a : Type) → a → <>' > ./not
Now let's try to prove a proposition like:
not(True) ⇒ False
The corresponding type is:
... which expands out to:
... and the value that has this type is:
Double negation
However, suppose we try to prove "double negation":
∀(a ∈ Prop): not(not(a)) ⇒ a
... which says that "if a is not false, then a must be true".
The corresponding type would be:
∀(a : Type) → ./not (./not a) → a
... which expands out to:
∀(a : Type) → ((a → <>) → <>) → a
... but there is no value in the Dhall language that has this type!
The reason why is that every type checker corresponds to a specific logic system and not all logic systems are the same. Each logic system has different rules and axioms about what you can prove within the system.
Dhall's type checker is based on System Fω which corresponds to an intuitionistic (or constructive) logic. This sort of logic system does not assume the law of excluded middle.
The law of excluded middle says that every proposition must be true or false, which we can write like this:
∀(a ∈ Prop): a ∨ not(a)
You can read that as saying: "any proposition a is either true or false". This seems pretty reasonable until you try to translate the proposition to the corresponding type:
∀(a : Type) → < Left : a | Right : a → <> >
... which in Haskell would be:
example :: Either a (a -> Void)
We cannot create such a value because if we could then that would imply that for any type we could either:
- produce a value of that type, or:
- produce a "counter-example" by creating
Void from any value of that type
While we can do this for some types, our type checker does not let us do this automatically for every type.
This is the same reason that we can't prove double negation, which implicitly assumes that there are only two choices (i.e. "true or false"). However, if we don't assume the law of the excluded middle then there might be other choices like: "I don't know".
Not all hope is lost, though! Even though our type checker doesn't support the axiom of choice, we can still add new axioms freely to our logic system. All we have to do is assume them the same way we assume other propositions.
For example, we can modify our original proposition to now say:
(∀(b ∈ Prop): b ∨ not(b)) ⇒ (∀(a ∈ Prop): not(not(a)) ⇒ a)
... which you can read as saying: "if we assume that all propositions are either true or false, then if a proposition is not false it must be true".
That corresponds to this type:
(∀(b : Type) → < Left : b | Right : b → <> >)
→ (∀(a : Type) → ((a → <>) → <>) → a)
... and we can create a value of that type:
λ(noMiddle : ∀(b : Type) → < Left : b | Right : b → <> >)
→ λ(a : Type)
→ λ(doubleNegation : (a → <>) → <>)
→ merge
{ Left = λ(x : a) → x
, Right = λ(x : a → <>) → merge {=} (doubleNegation x) : a
}
(noMiddle a)
: a
... which the type checker confirms has the correct type:
$ dhall
λ(noMiddle : ∀(b : Type) → < Left : b | Right : b → <> >)
→ λ(a : Type)
→ λ(doubleNegation : (a → <>) → <>)
→ merge
{ Left = λ(x : a) → x
, Right = λ(x : a → <>) → merge {=} (doubleNegation x) : a
}
(noMiddle a)
: a
<Ctrl-D>
∀(noMiddle : ∀(b : Type) → < Left : b | Right : b → <> >) → ∀(a : Type) → ∀(doubleNegation : (a → <>) → <>) → a
λ(noMiddle : ∀(b : Type) → < Left : b | Right : b → <> >) → λ(a : Type) → λ(doubleNegation : (a → <>) → <>) → merge { Left = λ(x : a) → x, Right = λ(x : a → <>) → merge {=} (doubleNegation x) : a } (noMiddle a) : a
You can read that proof as saying:
- The law of the excluded middle says that there are two possibilities: either
a is true or a is false
- If
a is true then we're done: we trivially conclude a is true
- If
a is false then our assumption of not(not(a)) is also false
- we can conclude anything from a false assumption, therefore we conclude that
a is true
What's neat about this is that the compiler mechanically checks this reasoning process. You don't have to understand or trust my explanation of how the proof works because you can delegate your trust to the compiler, which does all the work for you.
Conclusion
This post gives a brief overview of how you can concretely translate logical propositions and proofs to types and programs. This can let you leverage your logical intuitions to reason about types or, vice versa, leverage your programming intuitions to reason about propositions. For example, if you can prove a false proposition in a logic system, then that's typically an escape hatch in the corresponding type system. Similarly, if you can create a value of the empty type in a programming language, that implies that the corresponding logic is not sound.
There are many kinds of type systems just like there are many kinds of logic systems. For every new logic system (like linear logic) you get a type system for free (like linear types). For example, Rust's type checker is an example of an affine type system which corresponds to an affine logic system.
To my knowledge, there are more logic systems in academic literature than there are type systems that have been implemented for programming languages. This in turn suggests that there are many awesome type systems waiting to be implemented.