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.**

skip to main |
skip to sidebar
#
Concrete Mix

## Saturday, July 30, 2011

###
Moved

## Saturday, March 5, 2011

###
64-bit Version of WindowsWhere

## Saturday, October 2, 2010

###
Oleg's Unusual Polymorphism

*polymorphically*. In ML we can only
apply *monomorphically*, that is, to arguments of
a single type within the body of *inline* all possible projections that *and*
## Friday, October 1, 2010

###
SKI!

## Wednesday, September 22, 2010

###
Apologies

## I Am

## What's Come Before

## Labels

## Interlink

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`

`selector`

`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

`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`

`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!

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.

Subscribe to:
Posts (Atom)

mix
(15)
inference
(6)
mix inference
(3)
static
(2)
windowswhere
(2)
apology
(1)
shred
(1)
value-inference
(1)