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