SKI!

Note: I'm actually not much of a skier, being as I am more interested in sliding sideways...

So, a while ago I was wandering the halls of the internet and came across this fun post, an implementation of the SKI combinator calculus at the type level in Scala. So I asked myself, "would this work in Mix?" The answer is "yes", which causes me a bit of consternation given that I'd like to do type inference for Mix. But anyway, let's have a look.

First, what is SKI? It's a set of combinators S, K, and I, along with rules for evaluating or rewriting them, that happens to be equivalent, in some sense, to the untyped lambda calculus. Evaluating expressions composed of these combinators (and variables x, y, and so on) is pretty simple: I x evaluates to x, K x y evaluates to x, and S x y z evaluates to x z (y z). So, for instance, S K x y evaluates first to K y (x y) by the S rule, and then to y by the K rule. And S K I I evaluates to I by S and then K. Note that we can actually simulate I using, for example, S K K, so we can only consider S and K going forward.

The Scala encoding given in by Michid is fully at the type level. We define several classes: one for each combinator, and a few representing variables. Each class has a "member" type corresponding to application and evaluation. The former is parameterized by an "argument" type. So if we want to construct a type representing I x, and we have defined I and x, we simply access the "application" member type of I, parameterizing it with the type x: Ix = I#apply[x].

Next, if we want to evaluate it (and thereby get back x), we simply access the "evaluation" member type of Ix: x' = Ix#eval.

An important aspect of the implementation given is that it actually performs evaluation as it is possible. By this I mean that any time we try to apply a reducible term t to another s, as in t#apply[s], we first reduce t and only then access the member type of the result of the reduction. So all of the types that correspond to reducible terms have a definition for apply that looks like this:

    type apply[x <: Term] = eval#apply[x]

Apologies for the lack of Scala syntax highlighting.

It first evaluates itself by accessing its own eval, and then applys the argument by accessing apply member type of the result of evaluation, parameterized by x. And it results in types representing terms that, after construction, have only one thing left to reduce.

So, how does this play out in Mix? Quite nicely, in fact, because in Mix we don't need to lift all of our computation into the type level in the same way. In Scala we created part of a class hierarchy (Term, S, etc.) for implementing SKI, the same as we would have if we wanted to evaluate it at runtime. But we didn't write the revelant Apply and Evaluate methods; instead we reflected them as types. In Mix we will implement these methods as usual, and find that the inference algorithm will evaluate our code correctly at compile time. That is to say, we can reflect only our data as types, but implement our functions on that data as methods over instances of types:

    // Base term class with default implementations.
    class Term
    {
        Apply(z) { return new Application(this, z); }
        Eval() { return this; }
        operator+(z) { return this.Apply(z); }
    }
    
    // Applications
    class Application : Term
    {
        var x; var y;
        new(x, y){ this.x = x; this.y = y; }
        ToString() { return "(" + x + " " + y + ")"; }
    }
    
    // Our combinators: partial applications of combinators override
    // Apply; complete applications override Eval as well.
    class K : Term
    {
        Apply(x){ return new Kx(x); }
    }
    
    class Kx
    {
        var x;
        new(x){ this.x = x; }
        Apply(y){ return new Kxy(this.x, y)
        ToString(){ return "(K " + this.x + ")";
    }
    
    class Kxy
    {
        var x; var y;
        new(x, y){ this.x = x; this.y = y; }
        Apply(z){ return this.Eval().Apply(z); }
        Eval(){ return this.y; }
        ToString(){ return "(K " + this.x + " " + this.y + ")";
    }
    
    // And so on for S, Sx, Sxy, and Sxyz, as well as I and Ix.
        
    // Constants have a specialized ToString; we need separate
    // classes so we can distinguish between an Constant("C")
    // and Constant("D") at the type level.
    class Constant : Term
    {
        var name;
        new(name) { this.name = name; }
        ToString() { return this.name; }
    }
    
    class C : Constant
    {
        new() : Constant("C") {}
    }
    
    class D : Constant
    {
        new() : Constant("D") {}
    }

A few comments on the code itself. We use inheritance to build a term hierarchy, as you might find in C# or Java, giving default implementations of Eval and Apply, as well as of operator+ which is implemented in terms of the latter. We also define ToString for printing the results at runtime; note that we frequently make use of the fact that Mix.String.operator+ invokes ToString on its argument.

Next, a few comments on the intentions behind the code. The most important is that we must use a new class for each different constant we want to represent, so that the type of a term actually reflects the structure of the term. That is, when we write var x = new Application(new C(), new D()); we want that they type of x is something like Application<C, D>, written in a C#-like syntax. Next, we also ensure that instances of C and D are different at runtime in their value (that is, what is printed by ToString).

Now we can construct a combinator term and evaluate it. We'll evaluate S K I c to c. Unfortunately we need to ask Mix to print the type of the result of evaluating the term using some "internals", namely the as ? operator, which prints a term's inferred type. Then we print it out, demonstrating that we can evaluate at the type level, but we're also playing with value level data representations.

    var S = new S();
    var K = new K();
    var I = new I();
    var c = new C();
    var d = new D();
    
    Int main(String args)
    {
        var term = S + K + I + C;
        var result = term.Eval() as ?;
        IO.print(string(term) + " => " + result);
        return 0;
    }

When we compile it we would get something like this log message, if I had a prettier pretty-printer for types:

ski.mix(10) : Log : Expression 'term.Eval()' has type 'C'.

And there you have it: type inference (but not type checking, though that doesn't make much sense as we haven't a way to write down types with methods, classes, and so on) in Mix is undecidable. Should we care? Do you?

Note: I haven't actually tested this code in a while, as my current version of Mix is in the midst of a rewrite!