figure 11. Representation of λ-abstractions as scala function values (higher order abstract syntax).

trait Functions extends Base {
def lambda[A,B](f: Rep[A] => Rep[B]): Rep[A=>B]
def infix_apply[A,B](f: Rep[A=>B], x:
Rep[A]):
Rep[B]
}

As opposed to the earlier power example, an invocation fac(m) will not inline the definition of fac but will result in an actual function call in the generated code.

However, the HOAS representation has the disadvantage of being opaque: there is no immediate way to “look into” a Scala function object. If we want to treat functions in the same way as other program constructs, we need a way to transform the HOAS encoding into our graph representation. We can implement lambda(f) to call

reifyBlock { f(fresh[A]) }

which will unfold the function definition into a Block that represents the entire computation defined by the function. But eagerly expanding function definitions is problematic. For recursive functions, the result would be infinite, that is, the computation will not terminate. What we would like to do instead is to detect recursion and generate a finite representation that makes the recursive call explicit. However, this is difficult because recursion might be very indirect:

 

def foo(x: Rep[Int]) = { val f = (x: Rep[Int]) => foo(x + 1) val g = lambda(f) g(x)

}

Each incarnation of foo creates a new function f; unfolding will thus create unboundedly many different function objects.

To detect cycles, we have to compare those functions. This, of course, is undecidable in the general case of taking equality to be defined extensionally, that is, saying that two functions are equal if they map equal inputs to equal outputs. By contrast, the standard reference equality, which compares memory addresses of function objects, is too weak for our purpose:

def adder(x:Int) = (y: Int) => x + y adder( 3) == adder( 3)

false

However, we can approximate extensional equality by intensional (i.e., structural) equality, which is sufficient in most cases because recursion will cycle through a well-defined code path in the program text. Testing intensional equality amounts to checking whether two functions are defined at the same syntactic location in the source program and whether all data referenced by their free variables is equal. Fortunately, the implementation of first-class functions as closure objects offers (at least in principle) access to a “defunctionalized” data type representation on which equality can easily be checked. A bit of care must be taken though, because the structure can be cyclic. On the java virtual machine (JVM), there is a particularly neat trick. We can serialize the function objects into a byte array and compare the serialized representations:

 

serialize(adder( 3) ) == serialize(adder( 3) ) true

 

With this method of testing equality, we can implement controlled unfolding. Unfolding functions only once at the definition site and associating a fresh symbol with the function being unfolded allows us to construct a block that contains a recursive call to the symbol we created. Thus, we can create the expected representation for the factorial function above.

3. 1. Guarantees by construction Making staged functions explicit through the use of lambda enables tight control over how functions are structured and composed. For example, functions with multiple parameters can be specialized for a subset of the parameters. Consider the following implementation of Ackermann’s function:

 

def ack(m: Int): Rep[Int=>Int] = lambda { n => if (m == 0) n+ 1 else if (n == 0) ack(m− 1)( 1) else ack(m− 1)(ack(m)(n− 1) )

}

 

Calling ack(m)(n) will produce a set of mutually recursive functions, each specialized to a particular value of m. For ack( 2)(n), for example, we get

def ack_ 2(n: Int) = if (n == 0) ack_ 1( 1) else
ack_ 1(ack_ 2(n− 1) )
def ack_ 1(n: Int) = if (n == 0) ack_0( 1) else
ack_0(ack_ 1(n− 1) )
def ack_0(n: Int) = n+ 1
acc_ 2(n)

In essence, this pattern implements what is known as “polyvariant specialization” in the partial evaluation community. But unlike automatic partial evaluation, which might or might not be able to discover the right