Puzzle: the depth of a type (solution)

12 03 2008

In my previous post I asked for a function depth, which takes an argument of type M and returns its structural depth.

Here is my solution:

object Puzzle {
class M[T]

abstract class Rep[T] {
def eval: int
}

implicit def toRep0[T](k: T) = new Rep[T] {
def eval = 0
}

implicit def toRepN[T](k: M[T])(implicit f: T => Rep[T]) = new Rep[M[T]] {
def eval = f(null.asInstanceOf[T]).eval + 1
}

def depth[T <% Rep[T]](m: T) = m.eval def main(args: Array[String]) { println(depth(0)) println(depth(new M[int])) println(depth(new M[M[int]])) println(depth(new M[M[M[int]]])) } } [/sourcecode] This is the same technique as discussed in my articles on implicit double dispatch. The function depth is applicable to any argument of type T which is implicitly convertible to type Rep[T]. Rep[T] instances implement a function eval, which returns the depth of the type this instance is representing. There are two function for implicit conversions: toRep0 and toRepN. The toRep0 function is responsible for the base case where the structural depth of the type of its argument is 0. The eval function thus returns 0 in this case. The toRepN function is responsible for the other cases where a Mn + 1[T] has to be converted into a Rep[Mn + 1[T]] (Mk[T] stands for M[M[…[T]]] having structural depth k). toRepN takes an implicit parameter f itself. This parameter is a conversion function for converting a Mn[T] into a Rep[Mn[T]] which is used for constructing Rep[Mn + 1[T]]. Since we can convert types of structural depths 0 and types of structural depth n + 1 when given a Rep[T] for T having structural depths n, we can – by induction – convert types of any structural depth.

The implementation of eval in toRepN is implemented in terms of the eval method of Rep[T]. However to access Rep[T] we need to apply f to a T. Since we don’t have an instance of T and since the actual instance does not matter, we simply pass null casted to T.

The technique employed here is a special case of the Code Follows Type pattern. The general idea is not to re-implement the structure of types in code, but to re-use the inherent information carried by types. While in Java this is only possible to a limited degree, Scala’s implicit conversions enable this technique even for recursive structures.

Credits are due to Henry Ware for pointing me to this paper about Scala’s higher kinds. Towards the end of the paper the authors show how to encode the church numerals as Scala types. The encoding plays nicely with the depth function. So – as I mentioned before in a comment – this might be a first, gentle step towards meta-programming with Scala. However, there are certain limitations I guess. I will write more about this later.

Advertisements

Actions

Information

4 responses

13 03 2008
Erkki Lindpere

Pretty cool. I wouldn’t have figured this out myself. I think reified generics would make this easier and cleaner, though? I don’t know — I’ve haven’t really programmed enough in a language that has them (such as C#).

17 03 2008
Henry Ware

Excellent stuff. This is really neat.

17 03 2008
michid

Henry,

I also gave a try to the base2 encoding you proposed earlier. This works pretty well. The code is along the same lines as the depth function, only that an implicit conversion function for each digit is needed.

I also tried to take the Church encoding one step further by adding multiplication but without success so far. The problem is, that multiplication needs currying and I don’t know how to do this on the level of types (if it is possible at all).

18 04 2008
Meta-Programming with Scala Part I: Addition « Michid’s Weblog

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

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




%d bloggers like this: