Tuesday, June 23, 2009

Mobile Code in C# via Finally Tagless Interpreters

Awhile back I described an idea to transparently execute code server-side or client-side given the same program. I've finally gotten around to implementing this using my encoding for type constructor polymorphism in C#.

Here is an example you can run from the original paper showcasing exponentiation which can execute transparently either server-side or client-side. The server-side code is intentionally limited to bases less than 100 and exponents less than 20.

Here is some simplified code that defines an exponentiation function:
void Build<B, R>(B _)
where B : ISymantics<B>, new()
var e = _.Lambda<int, Func<int, int>>(
x => _.Fix<int, int>(self => _.Lambda<int, int>(n =>
_.If(_.Lte(n, _.Int(0)), () => _.Int(1),
() => _.Mul(x, _.Apply(self, _.Add(n, _.Int(-1))))))));

The parameter "_" is the tagless interpeter and it's type is ISymantics<B>, which defines the semantics of the language being interpreted:
/// <summary>
/// The abstract base class of a typed expression.
/// </summary>
/// <typeparam name="T">The type of the encapsulated expression.</typeparam>
/// <typeparam name="B">The brand of the interpreter that can interpret this expression.</typeparam>
public abstract class E<T, B> where B : ISymantics<B>, new() { }

/// <summary>
/// The interface for interpreters.
/// </summary>
/// <typeparam name="B">The brand of the interpreter. This should be unique for each interpreter.</typeparam>
public interface ISymantics<B>
where B : ISymantics<B>, new()
/// <summary>
/// Construct an integer.
/// </summary>
/// <param name="i">The integer value.</param>
/// <returns>An expression encapsulating the value.</returns>
E<int, B> Int(int i);

/// <summary>
/// Add two expressions.
/// </summary>
/// <param name="left">The left expression.</param>
/// <param name="right">The right expression.</param>
/// <returns>The sum of the two expressions</returns>
E<int, B> Add(E<int, B> left, E<int, B> right);


The code-behind for the .aspx page interprets this code twice, once with a LINQ-based compiler for server-side execution, and once with a JavaScript backend to generate the client-side program.

The client-side program depends on only one utility function to compute the fixed point of a given function:
function fix(f) {
return function self(x) { return f(self)(x); };

Clearly any programs written this way are fairly verbose, but it's fairly straightforward to define wrapper structs around E<T, B>, such as Eint, Ebool, etc., to provide overloaded operators such that embedded programs look almost like ordinary C#. The current ISymantics interface is also limited to single-arg functions, but it's possible to add more overloads to support multi-arg functions.

Of course, it's already possible to translate C# expressions to JavaScript if we write a LINQ expression visitor. However, LINQ expressions are in a sense more limited than operating on this lifted data type. For instance, it's not possible to translate a static function to JavaScript using LINQ expressions, but it is possible using the final tagless representation.

It's an open question whether such final tagless interpreters can be made usable enough for real programming. However, the techniques employed here, in particular the structure which enables semi-safe type constructor polymorphism, are definitely useful for other projects that require retargetable abstractions.

The full source code is available, and includes a simple C# evaluator, LINQ-based compiler, a JavaScript backend, and an interpreter that computes the depth of the expression tree, which was also an example in the tagless paper. Also included is a partially working partial evaluator. This proved the trickiest to implement, and the only remaining problem appears to be recursive partial evaluation.

As future work, the partial evaluator can be parameterized by the type of compiler, so it can partially evaluate managed code and JavaScript programs; it is currently needlessly tied to the managed code interpreter. I also plan to implement the aforementioned wrapper structs and other enhancements to improve the clarity of embedded programs, hopefully to the point where they are usable for real programming.

[Edit 2009-08-16: it just came to my attention that the JS failed on the first run, but succeeded after a server-side execution was performed. This was a DOM manipulation bug, and the source and server code have been updated to fix this.]