F# productization

Finally one of the most exciting pieces of news is out. Today it was announced that Microsoft intends to productize F#! F# is a functional language originating from the ML family (actually it's a close relation to OCAML) that was designed to be .NET language. It was designed and implemented by my colleague Don Syme in MSRC. Many congratulations to Don who has worked incredibly hard to get F# to the stage where it can be transferred over to the product team.

OOF not OOO

I've finally solved one of the Microsoft mysteries. No, not that one! Inside Microsoft people abbreviate the phrase "Out of office" as "OOF". In my three and a half years here I've not found anyone who could explain it. Catching up with Nadyne's blog, I've now discovered what it means. Somehow I feel better for knowing - I should get out more often I guess!

SQL code injection joke

A nice cartoon highlighting one of the problems addressed by Cw/LINQ can be found here. [Thanks to Nick Benton for spotting this!]

Zune 2.0

It's a tough time to be considering to buy a media player it seems. Everyone's seen the new Apple devices. Somewhat drowned in the noise, Microsoft also upgraded the Zune. There's a nice video here. Still single-touch, not multi-touch, but a much improved UI.

Mateja in the news!

My wife, Mateja Jamnik, was in the news last week in Slovenia. She attended a congress for Slovene scientists who work abroad. She ended up being rushed into the TV studios and being interviewed live on the 10 o'clock news - Odmevi - which is a very big TV slot in Slovenia.

If your Slovene is up to it - you can view the interview on the web. Go to this page and click the archive for 4th October 2007. This will launch a pop-up with an emedded player. There's about 3 minutes of introduction before you get to Mateja! What a star!

C# overloading

I just discovered an interesting "slip" in our ooPSLA paper. (Actually it's not a slip in the fragment of the language we consider, but it's dishonest in the Parnas sense (see an earlier blog entry)). I'm grateful to Eric Lippert for pointing this out to me.

Consider the process of typing a method call: e.m(f1,f2).

• First we synthesize a type for e, call it sigma.
• Next we generate a set, call it CMG, of all the candidate methods, i.e. the methods called m in sigma and its supertypes.
• Now we need to discover which one of these candidates are applicable: this amounts to checking that they have the same number of arguments as supplied (in this case 2), checking the modes (to handle ref parameters), checking that the arguments f1, f2 can be implicitly converted to the candidate argument types(*). [I'm ignoring generics here. If the method is generic and the call does not provide an explicit type argument list, then we need to use type inference to infer the type argument list]
• Finally we take this set and determine if there is a best method signature. [This is the heart of overloading resolution.]

Or that's what I thought happens! It turns out the last step is not strictly speaking true!!! It should be:

• Finally we take this set and the argument list and determine if there is a best method signature.

The problem arises because C# lets you define your own (cyclic) implicit conversions. Imagine we have two classes X and Y (that are not subtype related) but we define implicit conversions in both directions. Then imagine we have overloaded methods:

static void m(X x)
{
Console.WriteLine("Picked Program::m1");
}
static void m(Y y)
{
Console.WriteLine("Picked Program::m2");
}

and the code:

X x = null;
m(x);


C# picks the first "m" method because its the best match for the argument given that we know that argument of static type X. So overloading resolution needs to use this static type. As not every expression can synthesize a type, we have to pass the argument itself. If we had just considered the type signatures of the method m (i.e., X -> void and Y -> void) then neither would have been better and we would have rejected this call as ambiguous. Ha!

I'm currently extending our ooPSLA paper into a journal version. Part of this is formalizing the overloading process in C#. (It has been extended for C# 3.0 - it treats delegate types in/co-variantly.) Hence why I tripped over this.


(*) For some reason in the camera-ready copy this type check got missed out! Sorry - it was in the submitted version - I must have been too enthusiastic with my CTRL-ks when preparing the camera-ready copy :-(

POPL 2008

The paper with Matthew Parkinson on using separation logic to verify OO programs with inheritance got accepted for POPL 2008. Hurrah! We're currently working on an extended version that we should release in the next couple of months.

See you in San Francisco in January?