Moved

I've moved my blog (and more besides) to my new internet home at:

Zach Snow - That's Me

So head on over and check out the new digs if you like. This party's over.

64-bit Version of WindowsWhere

That's right, it turns out that WindowsWhere, a tiny program I wrote a while back to put Explorer windows in Windows 7 exactly where you want them, wasn't exactly 64-bit compatible. This is relatively unsurprising, given that I had no 64-bit install of Windows on which to test at that time. Now the only machine I have is a 64-bit one, and so I just had to get WindowsWhere working again.

Oleg's Unusual Polymorphism

I was wandering the internet, and stumbled once again across Oleg's page of O'Caml and other wizardry. One fun example was that of polymorphic selection.

The idea is that we (for whatever reason) want to be able to select data from a heterogenous structure in a particular way. In O'Caml one of our tools for storing such data is a tuple, so we'll take as input a pair of pairs. We want to be able to select either both of the fst elements, or both of the snd, using some function poly along with the selection function (either fst or snd):

    let data = ((1, 2), (3, 4))
        val data : (int * int) * (int * int)
    
    poly fst data
        - : int * int = (1, 3)
    poly snd data
        - : int * int = (2, 4)

So, how do we write poly? Here's our first attempt:

    let poly selector (l, r) = (selector l, selector r)
        val poly : ('a -> 'b) -> 'a * 'a -> 'b * 'b

    poly fst data
        - : int * int = (1, 3)
    poly snd data
        - : int * int = (2, 4)

Success! Or so we hope... but take a look at the type of poly. Not exactly what we were looking for; consider:

    let data' = (("1", 2), (3, "4"))
    
    poly fst data' (* Type error! *)

The essential issue is that, in the definition of poly, we are trying to use selector polymorphically. In ML we can only apply selector monomorphically, that is, to arguments of a single type within the body of poly. We actually want the type of poly to be something like:

    val poly : (forall a. b. (a, b) -> c) -> ((d * e) * (f * g)) -> {d * f when a = c, e * g when b = c}

Or something crazy like that (as Oleg mentioned, even with "real" polymorphism a la System F we cannot type poly the way we would like)... But it turns out that, if we are willing to do a bit of hackery we can get what we want:

    let poly selector (l, r) =
        selector ((fst l, fst r), (snd l, snd r))
             
        val poly : (('a * 'b) * ('c * 'd) -> 'e) -> ('a * 'c) * ('b * 'd) -> 'e

What we've had to do is inline all possible projections that selector can make, so that we can apply it just once (at one type). Incidentally, if you don't like the idea of invoking both fst and snd each time you want just one or the other, you could thunk it:

    let poly selector (l, r) =
        selector (fun () -> (fst l, fst r), fun () -> (snd l, snd r))
             
        val poly : ((unit -> ('a * 'b) * (unit -> 'c * 'd)) -> 'e) -> ('a * 'c) * ('b * 'd) -> 'e

Here you'll have to invoke poly with an extra argument:

    poly fst data' ()
        - : string * int = ("1", 3)

So, that's all just a recap of what Oleg wrote, and which I found quite interesting. But as I looked a bit more, things seemed strange. First, take a look at the type of the first argument to poly:

    val selector : ('a * 'b) * ('c * 'd) -> 'e

What does this mean? It's basically saying that selector can return anything it wants; that is, it's a whole lot less restrictive than the "crazy" type we wanted to write above. So poly works as we'd like when selector is either fst or snd. But its not a whole lot more useful than just writing out the whole thing longhand, as below, because defining any more selectors will require us to understand the internals of how poly operates (and also how our heterogenous data is structured, of course).

    let fst' ((a,b),(c,d)) = (a, c)
        val fst' : (('a * 'b) * ('c * 'd)) -> ('a * 'c)
    let snd' ((a,b),(c,d)) = (b, d)
        val snd' : (('a * 'b) * ('c * 'd)) -> ('b * 'd)

Nevertheless, we have solved the problem that we set out to solve, by first inlining (and thunking) all of the possible projections of our heterogenous data structure, and then applying our selector to the result. Oleg points out that this demonstrates the relationship that inlining has to polymorphism: essentially inlining allows us to "outside" the restrictive type system and check types only after expansion, which means we can seemingly abstract over aspects of a type that the type system itself cannot allow. This is played out to good effect in F# with its notion of inlining and statically resolved type parameters, though of course there the language actually does the inlining for you, and has extended the type system to make sense of it.

So anyway, what happens when we want to apply this to larger structures, perhaps without as much built-in "symmetry"? Let's add some extra data to our structure.

    type 'a 'b 'c 'd 'e heterogenous = ('a * 'b) * ('c * 'd) * 'e
    let poly selector (l, r, extra) = selector ((fst l, fst r, extra), (snd l, snd r, extra))    

So that works, fair enough. But still, it feels like there's something funny about our examples. It's almost like our structure isn't so heterogenous after all. What about this?

    type 'a 'b 'c 'd 'e heterogenous = ('a * 'b * 'c) * ('d * 'e)

Well now, what kind of selectors could we use on this data structure? There really aren't any yet (though of course we can write some). In fact, the only reason that we ran into trouble before is that we didn't want to write selectors for the data at hand, instead opting to try to use existing selectors on different pieces of the structure. We were exploiting some uniformity, some homogeneity, in the structure (namely that there were several pairs in the structure), and in fact we were able to capture this homogeneity using the type system (in spite of it, perhaps) after a fashion. But I wonder: How often you might run into this problem, where you don't, for whatever reason, want to write your own selectors over the structure in its entirety? Consider:

    let fst'' ((a,_,_),(b,_)) = (a, b)
    let snd'' ((_,a,_),(_,b)) = (a, b)
    let thr'' ((_,_,a),(_,_)) = a
    
    let poly selector data = selector data

Here poly just becomes apply, and of course our selectors understand the entirety of the structure. There wasn't any ready-made uniformity in the structure, so we did it all by ourselves. Of course, if could abstract over the length of tuples we would be in business again... Well, enough of that.

Note: I had to run before I could proofread this... apologies.

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!

Apologies

Apologies are once again in order. Things have been interesting, but not in a way that you'd enjoy, dear Reader. I use "interesting" in the very loosest of senses. I shall, however, endeavor to provide some sort of commentary on something or other, sooner rather than later.