read

This article is my give on the relationship between mathematical proofs and programming languages. Many details on specific implementation have been left out with the aim for clarity and conceptual coherency.

The source used in this article is available as a Gist.

Proofs and Programming

First, what is a proof? A proof is a series of deductive arguments, such that the proposition is justified. This description might seem quite abstract, so let us look at a concrete example using the Peano naturals for representing natural numbers.

As the proposition has no quantifiers, we can directly use the first argument to reduce the expression. That is, the one given by the usual definition of addition over Peano numbers. We then have the following expression.

We still have a mathematical object, a propositional claim. We know from the Peano axioms, that syntactical equivalence satisfies reflexivity, symmetry, and transitivity. Henceforth the properties of equality are satisfied, and we may end our deductive sequence.

Next, we want to translate above into programming.

In Haskell

From the Curry–Howard correspondence we know that propositions are types and proofs are programs. Alright, so we need to make an expression that has above expression as its type, and a program which inhabits this type.

First, we need to define our objects: Peano naturals and Equality. We implement Peano naturals the usual way. I elaborate on this in a previous post. Equality is defined as follows.

data Refl a b where
  Refl :: Refl a a

Evidently, we the value Refl can only inhabit the type Refl a b if the types a and b are identical. Concerning the Curry-Howard correspondence, the Refl value also has the unit type - it is not possible to attach further data to the constructor.

We have defined equality in terms of reflection. However, we need equality also to satisfy symmetry and transitivity. In the source, we have the code needed for that.

We now want to make the type1 for our proof, or, the equivalent to the proposition stated above:

onePlusOneEqualsTwo :: Refl (Add (S Z) (S Z)) (S (S Z))

The Add in the type definition is a type family defined in the source. It is defined as we would usually define addition over Peano naturals.

To prove it we need to make an inhabitant to that type. The program is very simple for this case as the Haskell compiler reduces the type level expression per semantics of type families.

onePlusOneEqualsTwo = Refl

As it compiles2 it shows that Haskell is content with the proof.

Quantifiers

We want to abstract our proofs. In proving terminology, we do this through quantifiers.

To have a more graspable problem that includes only quantification, without induction, we detour to boolean algebra. Here we can try to formalize De Morgan’s theorem:

here a and b can only assume two values, true and false.

deMorgan :: SBool a -> SBool b -> Refl (Not (And a b)) (Or (Not a) (Not b))
deMorgan STrue STrue   = Refl -- The first case
deMorgan STrue SFalse  = Refl
deMorgan SFalse STrue  = Refl
deMorgan SFalse SFalse = Refl

We simply provide an inhabitant to the type based on pattern matching. This is the same as proving by case analysis.

To understand what goes on we instantiate the type expression in each case. Afterward, the compiler reduces per the semantics of the Not, And, and Or type families. In the first case we instantiate the type expression such that.

deMorgan :: SBool Tru -> SBool Tru
    -> Refl (Not (And Tru Tru)) (Or (Not Tru) (Not Tru))

This instantiation is from the value STrue which has the type SBool Tru. The compiler then reduces the expression and derives that Refl :: Refl Fls Fls. From the interpreter, we get that.

*Proof> :t deMorgan STrue STrue
deMorgan STrue STrue :: Refl 'Fls 'Fls

Induction

Many interesting properties we want to reason about includes unbound data. That is, the data we think about is inductively defined. We now go back to the examples considering natural numbers as they are a good medium for discussing inductively defined data.

plus_id_r is the property that adding zero to n on the right side is the identity of n. plus_id_l is when we add 0 on the left side.

plus_id_l is given directly from our definition of addition. But plus_id_r needs to be proven, and we can do this inductively using following code.

plus_id_r :: forall n. SNat n -> Refl (Add n Z)  n
plus_id_r Zero = Refl
plus_id_r (Succ x) = gcastWith (plus_id_r x) Refl

The first case is the base case. We know that the value is Zero and hence we can derive the type to Z. It is immediately visible that Refl inhabits the type Refl Z Z.

The next case is the induction case. Here we fold out the value such that if n = Succ x, then x = n-1 - we reduce this on our argument. We justify that Refl also is an inhabitant in this case by calling plus_id_r on the reduced value.

Discussion

It is indeed possible to prove stuff in Haskell. But it is not further practical. The reason is in particular because the language is not designed with the constructions we need, such as dependent types. We simulate them through GADTs.

The closest languages to Haskell that are suited for this is languages such as Idris and Gallina (Coq). They have all the facilities needed for incorporating proofs into one’s code.

If one has a software development background firmly grounded in OOP (Java, C#), it requires quite some time to wrap one’s head around the new way to understand types.

That we can do above is mostly of academic interest: How do make sure that certain compilers indeed do what they should do etc. But the techniques are becoming steadily more accessible to all programmers.

New languages, like Idris, come with type constructions to formally reason about our software.

Final Remarks

First, thanks to Aslan Askarov for providing valuable feedback on this article. It has been incorporated to provide a more coherent article.

This article was a precursor for a presentation at a spare time teaching event at Aarhus university. Thanks to them for letting me host the presentation.

  1. We solely use prefix notation to simplify the syntax. 

  2. Well, we need to set some compiler flags to make sure that all cases are covered. 

Blog Logo

Mads Buch


Published

Image

Mads Buch

Technical articles

Back to Overview