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