Archive for February, 2008

Research update

I finished a draft of "Generalizing Parametricity Using Information-flow" for LMCS this past weekend. That should leave me with fewer distractions to work on something for ICFP.

My work on Featherweight Scala is moving along, sometimes more slowly than others. Other than the issues with singletons I have already discussed, one problem with the original definition of Featherweight Scala is that it did not truly define a subset of Scala proper – that is, there were many valid Featherweight Scala programs that were not valid Scala programs.

So I have been working on trying to get Featherweight Scala to be as close to a subset of Scala proper as is possible without making it far too complicated to be a useful core calculus. Some of this has involved changing the definition of Featherweight Scala. Some of this has involved lobbying for changes to Scala proper to make it more uniform (so far I've succeed with extending traits to allow value declarations to be overridden).

Through the whole process I've also been spending a lot of time typing things into the Scala interpreter to figure out how Scala proper treats them. For better or worse, I've actually managed to uncover a fair number of bugs in Scala proper doing this. I've almost reached the point where I treat it as a bit of a game: can I from thinking about the properties of the Scala type system come up with some corner case that will exhibit an unsoundness in the language (a ClassCastException, a NoSuchMethodException, etc.), or at least crash the compiler?

Last week I came up with a pretty nice one where I used the fact that Scala should not allow inheritance from singleton types to launder types in an unsafe fashion (now fixed in trunk!). Prior to that I came up with something fun where you could trick the compiler into letting you inherit from Nothing (which is supposed to be the bottom of the subtyping hierarchy). Today I got to thinking about Scala's requirements that paths in singleton types must be stable – all components of a path must be immutable. So for example in

  2. var x = 3
  3. val y : x.type = x // ill-typed

The path x is not stable because x is a mutable variable. However, Scala does allow lazy value declarations to be stable.

  2. var x = 3
  3. lazy val y = x
  4. val z : y.type = y // allowed, at present

Note that y is not evaluated until it is first needed, and in this case its evaluation involves a mutable reference. Furthermore, add into the mix that Scala also provides call-by-name method arguments (lazy values are call-by-need). So I started riffing on the idea of whether I could violate stability by changing the mutable reference between the definition of the lazy value, or a call-by-name argument, and its use. In retrospect, I am leaning at present towards the belief that there is no way this should be exploitable from a theoretical standpoint. That does not mean that the implementation is necessarily in alignment with theory, however. I did manage to hit upon a combination in my experiments that resulted in a NoSuchMethodException, so the exercise was not a complete letdown.

I should point out that these things do not really reflect on the quality of the Scala language as whole. It is a rich language that does not yet have a complete formal model, and as such, in the implementation process it can be easy to overlook some particularly perverse abuses of the language.


When sending messages by post would be faster

We have been experiencing a massive delay in all the scala-* mailing lists at EPFL, both the public and private lists. The admins are so worried about open relays, the firewall prevent us from having our lab's admin run the mailing lists on one of our servers. Of course, despite telling the central admins that this is a serious problem, it has just gone from bad to worse. Last week we were seeing delays of about an hour. The past day or two the delay seems to have hit something like at least twelve hours. That means if someone does a Subversion commit, we do not see the commit e-mail for at least twelve hours. The same goes with submissions to the bug tracking system, or even internal queries.

Arguably, it has been good for productivity in some ways.

Comments (2)

Focusing and higher-order abstract syntax

I figured I would take a few minutes to point out that Noam Zeilberger had an excellent paper in POPL this year on Focusing and higher-order abstract syntax. I've spent some time in the past trying to better understand Andreoli's material on focusing and Girard's* Ludics from the judgmental perspective that I became accustomed to in my formative years, but I never really came up with anything. I found Noam's computational interpertation of focusing quite pleasing.

One low tech solution that has really been helping my wrists lately is that I obtained adjustable height desk for my office. The desks that came with my office were definitely far too tall for me (even when my chair at its maximum height).

* Girard seems to have redecorated his website since I last visited.


Occupational hazards

My wrists are continuing to get worse. I am writing this using Dragon Naturally Speaking Preferred, but it is quite a struggle with the software.  I'm not sure whether I need a faster computer, or my enunciation is just terrible.  I certainly won't be  able to use it for typesetting or programming anytime soon. I'm not quite sure what to do now.  Wow I didn't actually have to correct that last sentence.  Or that one.  Sometimes I just get lucky, I suppose.

Comments (2)