Curry-Howard in Idris

idris_hands_on.md

Types are theorems, programs are proofs.

(The code examples here use idris https://www.idris-lang.org)

To augment testing with a finite number of inputs we write mathematical proofs that demonstrate their correctness on all possible inputs.

The programmer writes the proofs and the compiler checks the proofs as it builds the software.

New languages and tools are being developed. Agda, Coq and Idris for example that allow us to prove useful properties about programs in general-purpose programming languages.

To achieve this we need a richer type system than those found in normal industrial languages that we're familiar with.

We need types that we can talk about properties of a program. e.g for any list L, the reverse of the reverse of L is equal to L.

reverse : List a -> List a
reverse xs = ?reverse

reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse xs = ?reverseReverse_rhs

We'll need to expore this type system a bit, in a language called idris. The syntax won't be too unfamiliar to Swift and Kotlin programmers because they've all been influenced by Haskell syntax.

We have the usual types Int, String etc. In Java / Swift we can have Types that depend on Types. e.g List<String>.

In Idris, types can also depend on values. And this is crucial to prove interesting things. Let's first look at equality type for Nat.

OnePlusOneIsTwo : Type
OnePlusOneIsTwo = 1+1 = 2

This is a Type that represents the statement 1 + 1 = 2. Traditionally we think of this as a Boolean true or false. But we will think of this as a type which classifies the evidence that it's true. In the same way that Int classifies its members 1,2,3....

The equality type has constructor:

(=) : (x : Int) -> (y : Int) -> Type

We'll write these types as 1 = 1, 1 = 2, 1 = 3, 2 = 2 etc.

A value of the type a = b is a proof of equality, so not all of the types have values.

There's no evidence for 1 = 2 means there's no value of this type. 1 = 1 has evidence so it has value, we call Refl.

proofThatOnePlusOneIsTwo : OnePlusOneIsTwo
proofThatOnePlusOneIsTwo = Refl

What if we try to prove that one plus one is three.

OnePlusOneIsThree : Type
OnePlusOneIsThree = 1+1 = 3

proofThatOnePlusOneIsThree : OnePlusOneIsThree
proofThatOnePlusOneIsThree = Refl

Proofs are related to execution. For our proof to be valid our compiler has to check that proofThatOnePlusOneIsTwo actually produces the value it claims. Idris can check for termination - but cannot always guarantee this due to the Halting problem.

proofThatOnePlusOneIsThree : OnePlusOneIsThree
proofThatOnePlusOneIsThree = proofThatOnePlusOneIsThree

The compiler is happy with this but if we execute proofThatOnePlusOneIsThree we get an infinite loop. We need to check for termination to trust our proofs. Turing completeness is the enemy of reasoning.

Let's try something more challenging, proving statements about even and odd numbers.

Definition:

n is even if ∃ k ∈ ℕ such that n = k + k

Write this in Idris as:

data Even : Nat -> Type where
 MkEven : (half : Nat) -> (k = half + half) -> Even k

zeroIsEven : Even 0
zeroIsEven = MkEven 0 Refl

This pair of a value and a type that depends on the value is how we represent existental quantification. This is called a Σ-type.

Definition:

n is even if ∃ k ∈ ℕ such that n = k + k + 1

Write this in Idris as:

data Odd : Nat -> Type where
 MkOdd : (haf : Nat) -> (k = S (haf + haf)) -> Odd k

oneIsOdd : Odd 1
oneIsOdd = MkOdd 0 Refl

To provide evidence of the negation of a statement we have to provide evidence that the type associated with the statement has no values.

For example we know there's no evidence for 1 = 2 but there should be evidence for not (1 = 2). We express negation in types as a type (1 = 2) -> Void where Void is the empty type (i.e has no values).

We can provide evidence for this in idris as follows:

zeroIsNotOne : (Z = S Z) -> Void
zeroIsNotOne prf = absurd prf

where absurd is a function provided by idris that converts a value of t -> a to a value of a given that t is uninhabited (i.e has no values).

Idris already knows that some types are uninhabited (see doc: Uninhabited in the idris REPL for the full list). In particular it knows that 0 = S n is uninhabited for any n. For other types like 1 = 2 we can proceed by induction.

succIsInjective : S k = S j -> k = j
succIsInjective Refl = Refl

succNotEqual : (n : Nat) -> (n = S n) -> Void
succNotEqual Z prf = absurd prf
succNotEqual (S k) prf = let step = succNotEqual k in
                              step $ succIsInjective prf

To prove that zero is not odd we can use the same idea.

zeroIsNotOdd : Odd 0 -> Void
zeroIsNotOdd (MkOdd haf prf) = absurd prf

Idris requires a bit more convinving that 1 is not Even.

oneIsNotEven : Even 1 -> Void
oneIsNotEven (MkEven Z prf) = absurd $ sym prf
oneIsNotEven (MkEven (S k) prf) = absurd $ succIsInjective (trans prf (sym $ plusSuccRightSucc (S k) k))

Proof that one plus an even number is odd. Produce evidence for Odd (S k) given evidence for Even k.

onePlusEvenIsOdd : Even k -> Odd (S k)
onePlusEvenIsOdd (MkEven half prf) = MkOdd half (cong prf)

cong means congruence, expresses the fact that (a = b) => (f a = f b).

Proof that one plus an odd number is even. Produce evidence for Even (S k) given evidence for Odd k.

onePlusOddIsEven : Odd k -> Even (S k)
onePlusOddIsEven (MkOdd haf prf) = MkEven (S haf) ?onePlusOddIsEven_rhs_2

To prove this we need to prove the intermediate step:

haf + (S haf) = S (haf + haf)

Using plusSuccRightSucc haf haf:

S (haf haf) = haf + S haf

Using trans:

trans (k = S (haf + haf)) (S (haf + haf) = (haf + S (haf)) = (k = (haf + S (haf)))

onePlusOddIsEven : Odd k -> Even (S k)
onePlusOddIsEven (MkOdd haf prf) = MkEven (S haf) (cong (trans prf $ plusSuccRightSucc haf haf))

Now we prove one final statement:

allEvenOrOdd : (k : Nat) -> Either (Even k) (Odd k)
allEvenOrOdd Z = Left zeroIsEven
allEvenOrOdd (S k) = case allEvenOrOdd k of
                          (Left l) => Right (onePlusEvenIsOdd l)
                          (Right r) => Left (onePlusOddIsEven r)

This is an example of a function where the target type depends on the argument. Called a Π-type. Expresses universal quanitication.