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