Meta-Programming with Scala Part I: Addition

18 04 2008

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.

About these ads

Actions

Information

5 responses

30 07 2008
Meta-Programming with Scala Part II: Multiplication « Michid’s Weblog

[…] my last post I showed how to encode the Church numerals and addition on them with Scala’s type system. I […]

13 08 2008
Type-safe Builder Pattern in Java « Michid’s Weblog

[…] 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 […]

29 10 2008
Meta-Programming with Scala: Conditional Compilation and Loop Unrolling « Michid’s Weblog

[…] 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 […]

29 01 2010
Scala type level encoding of the SKI calculus « Michid’s Weblog

[…] 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 […]

18 06 2010
Type Level Programming: Equality « Michid’s Weblog

[…] 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 […]

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s




Follow

Get every new post delivered to your Inbox.

%d bloggers like this: