I've moved my blog (and more besides) to my new internet home at:
So head on over and check out the new digs if you like. This party's over.
I've moved my blog (and more besides) to my new internet home at:
So head on over and check out the new digs if you like. This party's over.
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.
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) -> 'eWhat 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 pair
s 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.
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!