Practical Church Numerals in Scala

In my previous post, in which I was looking for uses of Scala's type infix operator, the examples I found all had to do with Church Encoding of integers. One of them was even a practical application: type-safe units calculations. I investigate that application in this post.

Copyright Note: The code in this post is not covered by the LGPL.

The code in the Representation and Addition sections is taken almost verbatim from the paper "Towards Equal Rights for Higher-Kinded Types" by Moors, Piessens and Odersky, July 2007, so is a derivative of their published code and is thus under their Copyright, used here under Fair Use.

The code in the Alternate Approach and following sections is based on Jesper Nordenberg's type-safe Units code. That code is part of a more general package; my version is simpler and hopefully easier to understand. Since I am not a lawyer I don't know if my implementation is different enough to be considered a separate work. Whatever part of this work is considered a derivative of Jesper's work is thus covered by his Copyright and is used here under Fair Use. However, I was unable to find a copyright notice associated with Jesper's code. Because of this uncertainty and to avoid the possibility of promoting the distribution of Jesper's code without clear permission, I reserve all rights on whatever part of this code is not considered derivative.

Contents

• Theory
• Representation
• Addition
• An Alternate Approach
• Addition Revisited
• Negative Numbers
• Subtraction
• Units
• Multiple Units
• Limitations
• Summary

Theory

Using the Peano axioms, the natural numbers are defined by assuming the existence of zero and a successor function, where one is defined as the successor of zero, two is defined as the successor of one, etc. If we use s() for the successor function, we can write these Peano numbers numbers like this:

0 = 0
1 = s(0)
2 = s(s(0))
3 = s(s(s(0)))
4 = s(s(s(s(0))))

Douglas Hofstadter's Typographical Number Theory uses a similar scheme to define the numbers, but without parentheses (0, S0, SS0, SSS0, etc.).

The approach of using the repeated application of a function to represent numbers (and other values) was used by Alonzo Church to embed data in the lambda calculus. That technique is called Church Encoding, and that representation when used for the natural numbers is called the Church Numerals.

If we use the letter z to represent zero, the Peano numbers look like this:

0 = z
1 = s(z)
2 = s(s(z))
3 = s(s(s(z)))
4 = s(s(s(s(z))))

This is closer to the first formulation we give below.

We can then define addition of two Peano numbers recursively:

a + 0 = a
a + s(b) = s(a + b)

Here's how it works:

a + 1 = a + s(0) = s(a + 0) = s(a)
a + 2 = a + s(1) = s(a + 1) = s(s(a))

We will be using this approach to add our Church Numerals, so when we get to that point you might want to look back at these examples.

Representation

We are going to use Scala's type system to represent our numbers. First, we will go through the Church Encoding and addition as it is done in section 3.2 on page 16 of the paper "Towards Equal Rights for Higher-Kinded Types" by Moors, Piessens and Odersky, July 2007. As stated in that paper:

Scala's kinds correspond to the types of the simply-typed lambda calculus. This means that we can express addition on natural numbers on the level of types using a Church Encoding.

This same formulation is used by Michael Dürig in his implementation.

Zero is represented by a type parameter z and the successor function is represented by a higher-kinded type s[_] that takes one "argument", which can be either z or, recursively, s[_].

Given these type parameters, we define our number types as follows:

type _0[s[_],z] = z
type _1[s[_],z] = s[z]
type _2[s[_],z] = s[s[z]]
type _3[s[_],z] = s[s[s[z]]]

Compare this to the Peano numbers given above.

Addition

Continuing with the approach from "Towards Equal Rights For Higher Kinded Types" (referred to as "Equal Rights" in the rest of this post), given the above type definitions for the numbers _0, _1, etc., we can now define a plus operation. Our "operation" is really a higher-kinded type, where the two arguments are actually types. Our numbers are all of the form _X[s[_],z], so that is the format of the two arguments to our plus function, which we call m and n. We also add two more type arguments, s[_] and z, which are necessary to make this formulation work.

type plus[m[s[_],z], n[s[_],z], s[_], z] = n[s, m[s, z]]

We add class definitions for the z and s types, and create a + type infix operator:

abstract class Zero
abstract class Succ[a]
type +[m[s[_],z], n[s[_],z]] = plus[m, n, Succ, Zero]

Now we can add our number types. To be consistent with our previously defined numbers, we include the two type parameters in our definition. This allows us to use _4 in another addition expression. (The "Equal Rights" paper does not include these parameters.)

type _4[s[_],z] = _2 + _2

If you do all of the expansion for the _X types and the + operator, you will find that _2 + _2, _1 + _3, and _3 + _1 expand to the same type definition, which is Succ[Succ[Succ[Succ[Zero]]]].

//Sample of how + works; don't type this into Scala
_2 + _2
+[_2, _2]
+[s[s[z], s[s[z]]
plus[_2, _2, Succ, Zero]
_2[Succ, _2[Succ,Zero]]
Succ[Succ[_2[Succ,Zero]]]]
Succ[Succ[Succ[Succ[Zero]]]]

There are a couple of ways you can verify that the addition operator gives equivalent types. One way is to define a function that takes an argument of a specific type, and pass different argument types to it:

def test(x:_3[Succ,Zero]) = null
test(null.asInstanceOf[_3[Succ,Zero]])
test(null.asInstanceOf[_1+_2])
test(null.asInstanceOf[_2+_2])  //error

Alternatively, you can use the approach in the "Equal Rights" paper and define an Equals higher-kinded type that is only valid when given two types that are the same. Try the examples below and you will see that the compiler accepts the line when the two types are equal, and complains when they are different:

case class Equals[A >: B <: B, B]
Equals[_1[Succ,Zero],_1[Succ,Zero]]
Equals[_1[Succ,Zero],_2[Succ,Zero]]  //error
Equals[_1+_1,_2[Succ,Zero]]

So far most of the code in the above Representation and Addition sections is taken almost verbatim from the "Equal Rights" paper. This is all done using the standard Scala type system and features that have been in Scala for a while.

But there is another way to do this.

An Alternate Approach

In addition to higher-kinded types, Scala allows abstract types to be defined within classes or traits. These types can then be made concrete in a subclass. This mechanism can often be used as an alternative to parameterized types. This was the approach taken by Jesper Nordenberg in his type-safe Units class (discussed in a previous post), and I preferred that approach. The code below was inspired by Jesper's code (and may be covered by his Copyright, see the copyright note above).

As Jesper did, I wanted to be able to represent negative numbers as well as positive numbers, and I wanted to be able to subtract as well as add. We will get to negatives and subtraction later; let's start with our representation and addition using abstract types.

Note: this Scala code includes recursive type definitions, which requires a feature in the Scala compiler that is not in version 2.7.2. In order to execute the examples below, you will have to download one of the nightly snapshots (or build from source). To get a nightly snapshot, visit the Scala downloads page, follow the "Nightly Builds" link, download a nightly build file, unpack it, and run bin/scala -Yrecursion 1. I used scala-2.7.2.r16357-b20081027010143.tgz. To find out if your copy of scala includes the recursion option, run scala -Y with no other options.

We start by defining an abstract trait CInt representing a Church Numeral, a positive or negative integer. The CPos trait subtypes CInt to represent only positive numbers or zero.

trait CInt {
    type Succ <: CInt
}

trait CPos extends CInt

Next we define our zero and successor classes.

class CSucc[P <: CPos] extends CPos {
        //P is our predecessor
    type Succ = CSucc[CSucc[P]]
        //our successor is the second successor of our predecessor
}

final class _0 extends CPos {
    type Succ = CSucc[_0]
}

With the above code we can now define some Church Numerals:

type _1 = CSucc[_0]
type _2 = CSucc[_1]
type _3 = CSucc[_2]

The Succ type field within the classes allows us to specify the successor to a type by referencing the Succ inner type, an approach which we will use for addition:

type _1b = _0#Succ
type _2b = _1b#Succ
type _3b = _2b#Succ

We can verify that these two syntaxes produce equivalent types by using the Equals class we defined above:

Equals[_1,_1b]
Equals[_2,_2b]

Addition Revisited

We modify our classes to add an addition operator. The new code is shown in bold.

trait CInt {
    type Succ <: CInt
    type Add[N <: CInt] <: CInt
}

trait CPos extends CInt
    //No change to CPos, but we redefine because CInt changed,
    //so that you can cut and paste this block into the Scala interpreter.

class CSucc[P <: CPos] extends CPos {
    type Succ = CSucc[CSucc[P]]
    type Add[N <: CInt] = P#Add[N]#Succ
}

final class _0 extends CPos {
    type Succ = CSucc[_0]
    type Add[N <: CInt] = N
}

type +[N1<:CInt, N2<:CInt] = N1#Add[N2]

//_0 changed, so we redefine the numbers that are based on it
type _1 = _0#Succ
type _2 = _1#Succ
type _3 = _2#Succ

Note the similarity of the Add type to the recursive definition of addition given in the discussion of Peano numbers above: adding a number N to zero gives that number N, and adding a number N to the successor of P is equal to the successor of P plus N.

We can now add our Church Numerals together, which we can verify with our Equals class:

Equals[_2,_1+_1]
Equals[_3,_2+_1]

Negative Numbers

The Successor approach above only covers the positive numbers. We will use another series of Church Numerals to represent the negative numbers. Instead of a successor function, we will use a predecessor function. We will use the term "successor" always to mean the next most positive number, and "predecessor" always to mean the next most negative number. Thus our negative numbers are represented by repeated application of the predecessor function p on zero:

 0 = 0
-1 = p(0)
-2 = p(p(0))
-3 = p(p(p(0)))
-4 = p(p(p(p(0))))

To code this, we will add a new trait CNeg for negative numbers, a new class CPred to encode our negative Church Numerals, and a new abstract type Pred. Note that the predecessor code is all completely symmetric with the successor code: exchange CPred with CSucc, Pred with Succ, P with S, CPos with CNeg, and the numerals _1 etc with _M1 etc., and you end up with the same thing.

As above, changes are in bold, and we include the bits that have not changed so that you can just copy and paste this entire code block into the Scala interpreter.

trait CInt {
    type Succ <: CInt
    type Add[N <: CInt] <: CInt
    type Pred <: CInt
}

trait CPos extends CInt
trait CNeg extends CInt

class CSucc[P <: CPos] extends CPos {
    type Succ = CSucc[CSucc[P]]
    type Add[N <: CInt] = P#Add[N]#Succ
    type Pred = P
}

class CPred[S <: CNeg] extends CNeg {
    type Succ = S
    type Add[N <: CInt] = S#Add[N]#Pred
    type Pred = CPred[CPred[S]]
}

final class _0 extends CPos with CNeg {
    type Succ = CSucc[_0]
    type Add[N <: CInt] = N
    type Pred = CPred[_0]
}

type +[N1<:CInt, N2<:CInt] = N1#Add[N2]

type _1 = _0#Succ
type _2 = _1#Succ
type _3 = _2#Succ

type _M1 = _0#Pred
type _M2 = _M1#Pred
type _M3 = _M2#Pred

We can test addition of negative and positive numbers using Equals:

Equals[_M1+_M1,_M2]
Equals[_M1+_1,_0]
Equals[_1+_M3,_M2]

Subtraction

Subtraction is mostly symmetric with addition, except that in order to subtract from zero, we need to be able to take the negative of the value rather the using the value directly. Thus we add a Neg operation (using a type) along with the Sub type for subtraction. With Neg, we no longer need to define separate types for the negative numbers (_M1 etc. above), we can use the Neg type field of the corresponding positive number. Thus negative one is _1#Neg, negative two is _2#Neg, etc.

case class Equals[A >: B <: B, B]

trait CInt {
    type Succ <: CInt
    type Add[N <: CInt] <: CInt
    type Pred <: CInt
    type Sub[N <: CInt] <: CInt
    type Neg <: CInt
}

trait CPos extends CInt
trait CNeg extends CInt

class CSucc[P <: CPos] extends CPos {
    type Succ = CSucc[CSucc[P]]
    type Add[N <: CInt] = P#Add[N]#Succ
    type Pred = P
    type Sub[N <: CInt] = P#Sub[N]#Succ
    type Neg = P#Neg#Pred
}

class CPred[S <: CNeg] extends CNeg {
    type Succ = S
    type Add[N <: CInt] = S#Add[N]#Pred
    type Pred = CPred[CPred[S]]
    type Sub[N <: CInt] = S#Sub[N]#Pred
    type Neg = S#Neg#Succ
}

final class _0 extends CPos with CNeg {
    type Succ = CSucc[_0]
    type Add[N <: CInt] = N
    type Pred = CPred[_0]
    type Sub[N <: CInt] = N#Neg
    type Neg = _0
}

type +[N1<:CInt, N2<:CInt] = N1#Add[N2]
type -[N1<:CInt, N2<:CInt] = N1#Sub[N2]

type _1 = _0#Succ
type _2 = _1#Succ
type _3 = _2#Succ

As usual, we can verify our subtraction operation using Equals:

Equals[_2 - _1, _1]
Equals[_1 - _2, _1#Neg]
Equals[_1#Neg - _1, _2#Neg]
Equals[_2#Neg - _1#Neg, _1#Neg]
Equals[_1#Neg - _3#Neg, _2]

The last code section above with the traits and classes provides a complete definition of our Church Numerals. Now let's see how to use them for a practical application.

Units

We define a class that represents a value that has units of meters. We define arithmetic operators so we can add or subtract quantities of the same type, or multiply or divide quantities that may have a different power of Meters:

case class Meter[M<:CInt](value:Double) {
    def +(that:Meter[M]) = Meter[M](this.value + that.value)
    def -(that:Meter[M]) = Meter[M](this.value - that.value)
    def *[M2<:CInt](that:Meter[M2]) = Meter[M+M2](this.value * that.value)
    def /[M2<:CInt](that:Meter[M2]) = Meter[M-M2](this.value / that.value)
}

The type parameter M is a Church Numeral representing the power of the units, as shown by the following type definitions:

type Scalar = Meter[_0]
type Length = Meter[_1]
type Area = Meter[_2]
type Volume = Meter[_3]

We define an implicit conversion from Double to Scalar, which we need for expressions such as r*r*PI as used below. Unfortunately, if we attempt to use PI*r*r Scala does not find our implicit conversion.

implicit def toScalar(d:Double) = new Scalar(d)

We can now define some simple type-safe functions:

import java.lang.Math.PI
def circleArea(r:Length):Area = r*r*PI
def sphereSurfaceArea(r:Length):Area = r*r*4.*PI
def sphereVolume(r:Length):Volume = r*r*r*(4./3.)*PI

The operators in our Meter class are normal operators, so we test them with some value assignment statements and calls to our functions:

val x = new Length(5)
val y = new Length(6)
val z = new Length(2)
val a:Area = x*y
val v:Volume = a*z
circleArea(x)
sphereVolume(y)
sphereVolume(a)         //type error

Multiple Units

We could define types for Kilograms, Seconds and any other units as we did for Meter above, but what happens when we want to divide a Meter by a Second to get a speed value? In order to allow operations across units, we have to combine our units into one class. We will create a MKS class that allows us to combine meters, kilograms and seconds. It looks a lot like the Meter class, except that it has three type parameter slots, one for each of our units. While we are at it, we also add the six relational operators so that we can do type-safe comparisons of values.

case class MKS[M<:CInt, K<:CInt, S<:CInt](value:Double) {
    def +(that:MKS[M,K,S]) = MKS[M,K,S](this.value + that.value)
    def -(that:MKS[M,K,S]) = MKS[M,K,S](this.value - that.value)
    def *[M2<:CInt,K2<:CInt,S2<:CInt](that:MKS[M2,K2,S2]) =
        MKS[M+M2,K+K2,S+S2](this.value * that.value)
    def /[M2<:CInt,K2<:CInt,S2<:CInt](that:MKS[M2,K2,S2]) =
        MKS[M-M2,K-K2,S-S2](this.value / that.value)

    def ==(that:MKS[M,K,S]) = (this.value == that.value)
    def !=(that:MKS[M,K,S]) = (this.value != that.value)
    def > (that:MKS[M,K,S]) = (this.value >  that.value)
    def >=(that:MKS[M,K,S]) = (this.value >= that.value)
    def < (that:MKS[M,K,S]) = (this.value <  that.value)
    def <=(that:MKS[M,K,S]) = (this.value <= that.value)
}

Now we define our physical types in terms of MKS:

type Length = MKS[_1,_0,_0]     //meter
type Area = MKS[_2,_0,_0]       //square meter
type Volume = MKS[_3,_0,_0]     //cubic meter, or kiloliter
type Mass = MKS[_0,_1,_0]       //kilogram
type Time = MKS[_0,_0,_1]       //second
type Frequency = MKS[_0,_0,_1#Neg] //hertz
type Speed = MKS[_1,_0,_1#Neg]  //meter per second
type Acceleration = MKS[_1,_0,_2#Neg] //meter per second-squared
type Force = MKS[_1,_1,_2#Neg]  //newton
type Energy = MKS[_2,_1,_2#Neg] //joule
type Power = MKS[_2,_1,_3#Neg]  //watt

With these units, we can define physical constants and functions and do type-safe calculations.

val G = MKS[_3, _1#Neg, _2#Neg](6.673e-11) //gravitational constant
def gravitationalForce(m1:Mass, m2:Mass, r:Length):Force =
    (m1*m2/(r*r))*G

val earthMass = new Mass(5.9742e24)
val earthRadius = new Length(6.378137e6)
val earthSurfaceAcceleration:Acceleration =
    (earthMass/(earthRadius*earthRadius))*G

Limitations

Jesper's implementation of type-safe units, on which this code is based, includes slots for length, mass and time as I have in my MKS implementation above, as well as for the other four accepted SI units current, temperature, molarity and brightness. This allows for a greater combination of units than my MKS implementation, so is more powerful and will cover most typical physical calculations. But even with all of those additional units, there may be some other unit that I want to add, such as radians of angle, or electron volts, or dollars. It would be nice if it were possible to define a new unit type and have it automatically work with the others, but I don't know how to do that with this setup. If I figure that out, it will have to be a subject for another post.

Summary

We have shown an implementation of Church Numerals and addition in Scala's type system using parameterized types, and another implementation using type variables. We extended the second implementation to include subtraction and negation as well as addition, then used those Church Numerals to define a class that can represent a collection of units with various powers on each unit. That class can be used to create unit-typed values and function definitions with which we can do type-safe calculations. Although we don't have an easy way to add arbitrary new units, a type-safe units class with the seven standard SI units can be used to do many calculations of physical quantities.

My thanks to Moors, Piessens and Odersky for their "Equal Rights" paper and to Jesper Nordenberg for his implementation of a type-safe units class.