A while ago I blogged about using Agda to prove the parity of added numbers. I’ve recently been doing some work on Idris and wondered how easy it would be to translate my Agda proof to Idris.

The original Agda code looked something like this:

module EvenOdd where

open import Data.Nat

data Even : ℕ → Set where
  evenZero : Even 0
  evenSuc : {n : ℕ} → Even n → Even (suc (suc n))

_e+e_ : {n m : ℕ} → Even n → Even m → Even (n + m)
evenZero e+e b = b
evenSuc a e+e b = evenSuc (a e+e b)

The direct Idris translation looks like:

module EvenOdd

data Even : Nat -> Type where
  evenZ : Even Z
  evenS : Even n -> Even (S (S n))

total
ee : Even n -> Even m -> Even (n + m)
ee evenZ m = m
ee (evenS n) m = evenS (ee n m)

The few differences:

• We don’t have to import a Nat type

• Totality is not the default (there is a flag to make it so, though)

• We can’t define mixed letter and symbol operators

Pretty easy! Time for something trickier. Now, I haven’t done very much type level Haskell but I wanted to see how easy it would be to translate to the recent GHC 7.8 release.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}

module EvenOdd where

data Nat = Z | S Nat

data Even :: Nat -> * where
  EvenZ :: Even Z
  EvenS :: Even n -> Even (S (S n))

type family Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z m = m
type instance Plus (S n) m = S (Plus n m)

ee :: Even n -> Even m -> Even (Plus n m)
ee EvenZ m = m
ee (EvenS n) m = EvenS (ee n m)

Getting a bit trickier. We’ve had to do the following:

• Enable data type promotion, so that data types can be kinds

• Enable type families, so we can write a type level functions

• Define our own Nat and use that as a kind

• Define our own Plus type level function (the type family)

• Get totality results as warnings (or errors via -Wall)

The few problems are caused by Haskell’s distinction between values, types and kinds. Everything else looks extremely similar - we’ve been lucky to fall into an area where the GHC data kinds extension works really well and we can promote our simple Nat type to a kind.

Let’s step it right up. Now let’s encode this in Scala. Are you ready?

package org.brianmckenna.evenodd

sealed trait Nat
trait Z extends Nat
case object Z extends Z
case class S[N <: Nat](n: N) extends Nat

sealed trait Even[N <: Nat]
trait EvenZ extends Even[Z]
case object EvenZ extends EvenZ
case class EvenS[N <: Nat](n: Even[N]) extends Even[S[S[N]]]

object Even {
  implicit val evenZ = EvenZ
  implicit def evenS[N <: Nat](implicit even: Even[N]) = EvenS[N](even)
}

sealed trait Plus[N <: Nat, M <: Nat] {
  type Result <: Nat
}

object Plus {
  type Aux[N <: Nat, M <: Nat, R <: Nat] = Plus[N, M] {
    type Result = R
  }

  implicit def plusZ[M <: Nat] = new Plus[Z, M] {
    type Result = M
  }

  implicit def plusS[N <: Nat, M <: Nat](implicit plus: Plus[N, S[M]]) = new Plus[S[N], M] {
    type Result = plus.Result
  }
}

object ee {
  def apply[N <: Nat, M <: Nat, R <: Nat](n: Even[N], m: Even[M])(implicit sum: Plus.Aux[N, M, R], re: Even[R]) = re
}

Now, this probably looks pretty verbose since we have to define our own type level Nat and Plus function. The type level Plus uses Scala’s path-dependent types.

What’s interesting is that our theorem is expressed as a constraint that given Even[N] and Even[M] then we can construct an Even[N + M] from an implicit. What we’ve given up is a constructive proof that every combination of two even numbers always results in an even number (but we know from our previous proofs that it’s true) - specifically, we can’t tell if the the implicit re can be found for all values. We could fix this by splitting the implicit up into each case but we can’t get totality checking.

Hopefully this gives a very quick feel for programming at the type level in Agda, Idris, Haskell and Scala. Type level programming in Agda and Idris is just as easy as programming at the value level. Type level programming in Haskell and Scala is a bit annoying, we have to write functions very differently at the type level and value level, but it’s impressive that we can achieve our goal in much more widely used languages.

Thanks to Miles Sabin for help with simplifying the Scala version.