In my previous post about Meta-Programming with Scala I suspected that there was no way to express partial function application in Scala’s type system. However Matt Hellige proofed me wrong in his comment.

His solution uses a trait for partially applying a function to some of its arguments. An abstract type exposed by the trait represents the resulting function which takes the remaining arguments.

object Partial {
// Partial application of f2 to x
trait papply[f2[_, _], x] {
type f1[y] = f2[x, y]
}
// apply f to x
type apply[f[_], x] = f[x]
trait X
trait Y
trait F[A1, A2]
// Test whether applying the partial application of
// F to X to Y equals in the type F[X, Y]
case class Equals[A >: B <: B, B]
Equals[apply[papply[F, X]#f1, Y], F[X, Y]]
}

Having this solved we can define a type which encodes multiplication on the Church Numerals.

trait curry[n[_[_], _], s[_]] {
type f[z] = n[s, z]
}
// Multiplication for this encoding
type mult[m[_[_], _], n[_[_], _], s[_], z] = m[curry[n, s]#f, z]

A full working example is available from my code page. Note, the code takes forever (i.e. some minutes) to compile. Matt also noted an issue with squares. With my version of the compiler (Ecipse plugin 2.7.2.r15874-b20080821120313) the issue does not show up however.

### Like this:

Like Loading...

*Related*

Meta-Programming with Scala: Conditional Compilation and Loop Unrolling « Michid’s Weblog(23:44:15) :[...] 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 Scala still [...]

Scala type level encoding of the SKI calculus « Michid’s Weblog(17:58:58) :[...] 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 [...]

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