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.

Daniel Spiewak(04:46:28) :The ability to encode Church Numerals in Scala still seems uselessly academic to me, but cool none-the-less. 🙂 Scala’s type system is impressively powerful, but as this post shows, it does have its limits. For me, the fact that it is not possible to define recursive types is rather annoying. Granted, it’s not a requirement which comes up very often, but it is certainly bothersome when it does.

michid(08:07:06) :@Daniel: Encoding Church Numerals in Scala’s type system is by itself pure academic. However, my intention was to use it as a starting point to go further from there: if it had worked out, one might have come up with an general encoding of some class of functions (most probably the primitive recursive functions). While this again is academic, it would give a clear picture of what the type system is capable of. It might have ultimately lead to constructs similar in power to those used in C++ template meta programming (which to me seems rather esoteric than academic 😉 ).

Matt Hellige(19:15:52) :Actually, you can sort of partially apply types, but you need to use a hack:

trait apply1[t[_[_],_],u[_]] {

type It[a] = t[u,a]

}

Notice that this needs to be defined for the specific kinds at which you intend to use it. (That is, if t and u had different kinds, one would need a different definition of apply1.) Then, we can write mul:

type mul[m[s[_], z], n[s[_], z], s[_], z] = m[apply1[n,s]#It, z]

This does work in at least some cases:

type x[m[s[_], z], n[s[_], z]] = mul[m, n, Succ, Zero]

println(depth(nullval[_3 x _2]))

This takes ages to compile, but when it’s done, it prints 6. Unfortunately, the same thing with

`_2 x _2`

blows up badly (and breaks otherwise working code in the same file). I have no idea why… Probably I’ll post to the list about it.(I can’t preview this comment, I guess. I hope the code comes out ok.)

Landei(20:03:13) :This is a very simple but useful example for the use of recursive types, written in Java:

http://javatuple.com/

The used technique allows to define Tuples of arbitrary arity. It is probably not very efficient, and I doubt anyone needs more than Tuple22 in Scala, but it shows that this kind of stuff is not only “academic”.

Meta-Programming with Scala Part III: Partial function application « Michid’s Weblog(22:35:16) :[…] with Scala Part III: Partial function application 27 08 2008 In my previous post about Meta-Programming with Scala I suspected that there was no way to express partial function […]

Meta-Programming with Scala: Conditional Compilation and Loop Unrolling « Michid’s Weblog(23:41:58) :[…] 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 Numerals in […]

Type Level Programming: Equality « Michid’s Weblog(16:14:28) :[…] Programming: Equality 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 […]