Proving Parity in Idris

Idris is a pure functional programming language with dependent types. In this post I am giving an example by David Christiansen on proving a parity theorem (or property) in Idris. The theorem states that every natural number is either even or odd. The example below demonstrates how to do theorem proving with a functional programming language such as Idris. It relies on equality expressed at the type level, which is possible thanks to dependent types. With that, Idris stands in stark contrast to languages such as Scala, where equality is broken. In the example, allEvenOrOdd k is a proof for every natural number k.

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

zeroEven : Even 0
zeroEven = MkEven 0 Refl

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

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

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

allEvenOrOdd : (k : Nat) -> Either (Even k) (Odd k)
allEvenOrOdd Z = Left zeroEven
allEvenOrOdd (S k) = case allEvenOrOdd k of
                       Left l => Right $ evenSOdd l
                       Right r => Left $ oddSEven r

Leave a Reply

Your email address will not be published. Required fields are marked *

IMPORTANT! To be able to proceed, you need to solve the following simple math (so we know that you are a human) :-)

What is (4 - 3] + 200?
Please leave these three fields as-is: