Copyright Note:The code in this post isnotcovered 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:

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

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:

This is closer to the first formulation we give below.0 = z 1 = s(z) 2 = s(s(z)) 3 = s(s(s(z))) 4 = s(s(s(s(z))))

We can then define addition of two Peano numbers recursively:

Here's how it works:a + 0 = a a + s(b) = s(a + b)

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.a + 1 = a + s(0) = s(a + 0) = s(a) a + 2 = a + s(1) = s(a + 1) = s(s(a))

### 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:

Compare this to the Peano numbers given above.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]]]

### 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.We add class definitions for the z and s types, and create atype plus[m[s[_],z], n[s[_],z], s[_], z] = n[s, m[s, z]]

`+`

type infix operator:
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.)abstract class Zero abstract class Succ[a] type +[m[s[_],z], n[s[_],z]] = plus[m, n, Succ, Zero]

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 istype _4[s[_],z] = _2 + _2

`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://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]]]]

Alternatively, you can use the approach in the "Equal Rights" paper and define andef test(x:_3[Succ,Zero]) = null test(null.asInstanceOf[_3[Succ,Zero]]) test(null.asInstanceOf[_1+_2]) test(null.asInstanceOf[_2+_2]) //error

`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:
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.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]]

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.

We start by defining an abstract traitNote: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.

`CInt`

representing a Church Numeral, a positive or negative integer.
The `CPos`

trait subtypes `CInt`

to
represent only positive numbers or zero.
Next we define our zero and successor classes.trait CInt { type Succ <: CInt } trait CPos extends CInt

With the above code we can now define some Church Numerals: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] }

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

`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:
We can verify that these two syntaxes produce equivalent types by using the Equals class we defined above:type _1b = _0#Succ type _2b = _1b#Succ type _3b = _2b#Succ

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

### Addition Revisited

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

Note the similarity of thetrait CInt { type Succ <: CInttype 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

`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:To code this, we will add a new trait0 = 0 -1 = p(0) -2 = p(p(0)) -3 = p(p(p(0))) -4 = p(p(p(p(0))))

`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.

We can test addition of negative and positive numbers using Equals:trait CInt { type Succ <: CInt type Add[N <: CInt] <: CInttype Pred <: CInt} trait CPos extends CInttrait CNeg extends CIntclass CSucc[P <: CPos] extends CPos { type Succ = CSucc[CSucc[P]] type Add[N <: CInt] = P#Add[N]#Succtype 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 CPoswith CNeg{ type Succ = CSucc[_0] type Add[N <: CInt] = Ntype Pred = CPred[_0]} type +[N1<:CInt, N2<:CInt] = N1#Add[N2] type _1 = _0#Succ type _2 = _1#Succ type _3 = _2#Succtype _M1 = _0#Pred type _M2 = _M1#Pred type _M3 = _M2#Pred

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.
As usual, we can verify our subtraction operation using Equals:case class Equals[A >: B <: B, B] trait CInt { type Succ <: CInt type Add[N <: CInt] <: CInt type Pred <: CInttype 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 = Ptype 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

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.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]

### 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:The type parametercase 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) }

`M`

is a Church Numeral representing the
power of the units, as shown by the following type definitions:
We define an implicit conversion fromtype Scalar = Meter[_0] type Length = Meter[_1] type Area = Meter[_2] type Volume = Meter[_3]

`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.
We can now define some simple type-safe functions:implicit def toScalar(d:Double) = new Scalar(d)

The operators in ourimport 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

`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.
Now we define our physical types in terms ofcase 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) }

`MKS`

:
With these units, we can define physical constants and functions and do type-safe calculations.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

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.

## 2 comments:

How would you handle something like square root, which is very common in physical formulas? You would have to divide the unit counter for each unit by two.

I guess you can do complete rational numbers using church numerals, but it could get very complex.

As you say, you could divide the number of every unit counter by two. It might be an interesting exercise to implement a divide-by-two using this encoding of Church Numerals - in general, integer division using Church Numerals can be done - but it would probably be messy.

You should not need to deal with rational numbers in the Church Numerals. While there are square roots in physical formulas, I don't think you ever end up with a fractional physical dimension, so if the unit counter dividend is not a multiple of two, you could make that an error.

Post a Comment