Meta-Programming with Scala Part II: Multiplication

This was sitting on my desk for quite a while now while I was busy with other things. Finally I came around to write things up.

In my last post I showed how to encode the Church numerals and addition on them with Scala’s type system. I mentioned that this approach does not seem to scale. In this post I show the problems I faced while I tried to extend the approach to multiplication. This particular example shows that Scala’s type system does not seem to support partial function application which in general is crucial for defining more complex functions base on simpler ones. But before delving into Scala, let’s review the church numerals in lambda calculus.

Define a lambda term for each natural number n

 

where stands for the n-fold application of s. Think of s standing for successor and z for zero. Then the number n is simply the n-fold successor of zero.

Addition can now be define as

.

Here the n-fold successor of zero is used as zero element for m. Again this can be thought of as the m-fold successor of the n-fold successor of zero.

Multiplications is similar but instead of using a different value for zero, a different successor function is used:

This boils down to the m-fold application of the n-fold successor function.

As in my previous post the Church numerals are encoded in Scala’s type system 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]]]
type _4[s[_], z] = s[s[s[s[z]]]]

I did not succeed encoding multiplication however. The most straight forward encoding – which closely follows the one for addition – looks like this

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

However the Scala compiler complains:

  s[_$1] forSome { type _$1 } takes no type parameters, 
  expected: one

Unlike addition, we need to pass a partially applied function here – namely the n-fold successor function. Since the above does not work, I’m not sure if there even is a syntax for expressing partial function application in Scala’s type system.

In another approach I tried to introducing a formal parameter for the n-fold successor function:

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

The compiler does not complain here which is encouraging. However this breaks on application

abstract class Zero
abstract class Succ[T]

type zero = mul[_0, _0, Succ, Zero] 
type one = mul[_1, _3, Succ, Zero] 

The first application results in a kind error

the kinds of the type arguments (Meta._0,Meta._0,Meta.Succ,Meta.Zero) do not conform to 
the expected kinds of the type parameters (type m,type n,type s,type z).
Meta._0's type parameters do not match type m's expected parameters: 
type s has one type parameter, but type n has two	

The second application causes an assertion failure of the Scala compiler (see Ticket #742).

For a better understanding let’s analyze what mul[_1, _3, Succ, Zero] expands to:

mul[_1, _3, Succ, Zero] =
_1[_3, Zero] =
_3[Zero]

While this looks somewhat correct, it is certainly not. _3 takes two arguments but gets one. This is exactly what the Scala compiler was complaining about.