In the solution to a puzzle I posted earlier, I mentioned that the taken approach might be a first step towards meta-programming in Scala.

While the approach to determine the depth of a type plays nicely with the Church encodings of natural numbers proposed in the paper Towards Equal Rights for Higher-kinded Types, defining arbitrary arithmetic operators seems problematic. Addition does not pose a problem. But there seems to be no easy generalization to other arithmetic operators. This is despite the fact that the authors of the above paper mention that Scala’s kinds correspond to the types of the simply typed lambda calculus.

In this post I will explain how to represent the natural numbers and an addition operator using Scala’s type system. In a later post I will show why this approach does not easily scale to the other arithmetic operators like multiplication and why I think that this might not be a problem of Scala’s type system in general but rather a shortcoming of its syntax. Finally I noted that Scala 2.7.1.RC1 dropped the contractiveness requirement for implicits. This might open up another way for meta-programming. I probably write more on this in yet another post.

The following code shows a Church encoding of the natural numbers in Scala’s type system. (The full source is available from my code page).

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

A natural numbers is encoded as a type function which takes two arguments: a successor function and a zero element. The *n*-th natural number is then the *n*-fold application of the successor function to the zero element. Such natural numbers can be instantiated by passing them an actual type for its successor function and its zero element. The *depth* function form my last post can then be used to evaluate such a number;

abstract class Zero abstract class Succ[T] type two = _2[Succ, Zero] println(depth(nullval[two])) // prints 2

We can now define an addition operator like this:

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

Basically *plus* takes two Church numerals *n* and *m* and composes them such that *m* becomes the zero element of *n*. The second line defines an infix *+* operator:

println(depth(nullval[_2 + _2])) // prints 4 println(depth(nullval[_2 + _3])) // prints 5

Let’s analyze in detail what *_2 + _3* expands to in order to better understand above code:

_2 + _3 = plus[_2, _3, Succ, Zero] = _3[Succ, _2[Succ, Zero]] = _3[Succ, Succ[Succ[Zero]]] = Succ[Succ[Succ[Succ[Succ[Zero]]]]]

So passing *_2 + _3* to the *depth* function will indeed print *5* since this its structural depth.

From here one might want to generalize this to other arithmetic operations. I tried multiplication but failed so far. In a next post I will explain my closest shot(s) at multiplication and I will explain what I think are the difficulties with this approach.

Meta-Programming with Scala Part II: Multiplication « Michid’s Weblog(21:08:05) :[…] my last post I showed how to encode the Church numerals and addition on them with Scala’s type system. I […]

Type-safe Builder Pattern in Java « Michid’s Weblog(21:00:39) :[…] Builder Pattern in Java 13 08 2008 In this post I deviate a bit from the topic of my recent posts about Meta-Programming with Scala. I will have more to say about the latter topic in upcoming […]

Meta-Programming with Scala: Conditional Compilation and Loop Unrolling « Michid’s Weblog(23:39:01) :[…] Compilation and Loop Unrolling 29 10 2008 The kind of comments I keep getting on my static meta-programming with Scala blogs are often along the lines of: “The ability to encode Church […]

Scala type level encoding of the SKI calculus « Michid’s Weblog(17:58:49) :[…] is capable of. Various of my older posts show how Scala’s type system can be used to encode addition and multiplication on natural numbers and how to encode conditions and bounded […]

Type Level Programming: Equality « Michid’s Weblog(16:14:34) :[…] 18 06 2010 Apocalisp has a great series on Type Level Programming with Scala. At some point the question came up whether it is possible to determine equality of types at run […]