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)

Tablet computing

Writing about RSI reminded me that I had never gotten around to talking about the ThinkPad X61 tablet I purchased at the beginning of August. It is a pretty solid when used as a laptop.

As far as being a tablet goes, it works reasonably well in that domain too, with some exceptions. Firstly, for now if you want to use the tablet capabilities to their fullest, you need to run Windows Vista. The tablet is supposed to be supported under Linux, but there is really only one program that supports handwriting recognition program available, Cellwriter. It looks promising, particularly because it can be trained to generate any Unicode glyph – with Vista you are limited to the system's configured language. However, I do not think it would be difficult for Gnome or KDE to catch up in this area if they put a little effort into it.

My initial solution to this was that I would just run Linux under VMWare. Except I soon found that while I can use the tablet as a mouse, VMWare will not accept the input events the handwriting recognition subsystem generates. When I filed this as a bug they did not seem to think this was a problem.

While working with standard Windows applications, anything with a input field can accept handwriting recognition input. I almost wrote my entire defense presentation this way, but near the end I gave in and used the keyboard to do most of the last minute tweaking.

Of course, there is the question of whether writing by hand is any easier on my wrists than typing. It is difficult to say, for one, it becomes basically impossible to use emacs, unless you can do everything from pull-down menus, because of the chording necessary to activate some functionality. And it is definitely slower than typing, even with practice I expect. However, part of the problem could perhaps be resolved by rethinking various applications with tablets in mind.


Research update

I have been making reasonably steady progress on my formalization of Featherweight Scala in Coq. I have just about seven hundred lines of definitions, with only few more things to make explicit. At that point I should be ready to start on actually proving progress and preservation.

I volunteered to triage issues submitted to the Scala bugtracking system this month, so that has been taking a little bit of my time. Mostly this just involves checking that what was submit is truly a bug and reproducible, before assigning it to the relevant person.

I am also responsible for the interpreter and the ScalaDoc, so I have also spent the time fixing a few bugs that have shown up in the interpreter. The big one of the past week is that for 2.6.2 the plan is to finally interoperate with Java generics. As a consequence, the compiler now defaults to generating class files in the format used in version 1.5 of the JVM and above. However, this broke the nightly tests run against the 1.4 JVM. The interpreter would compile and run fine until it tried to load one of the class files itself had compiled, which had an incompatible version number. So I added a check that if the interpreter is running on a pre-1.5 JVM, to force it to generate compatible class files.

An undergrad e-mailed me to ask about working on the Literate Scala semester project that I had posted. I met with him briefly last week for mostly administrative purposes. That should be interesting.

I should be moving forward on the implementation of virtual classes, but I have been avoiding it because I am not yet sure how to best modify the AST to represent them. I will hopefully have chance to discuss it with Martin this week.

I have also been spending time thinking about the next major project, an effect system for Scala. I have been thinking hard about how to add one while still maintaining reasonable backward compatibility and so that it is not exceedingly verbose. It is a very difficult problem. Furthermore, one of the most widely used effect systems that exists in programming languages, Java's throws clauses, is generally reviled by programmers. One thought I had was that maybe a whiz-bang effect system with effect polymorphism, a rich language of effects, and hooks for adding user defined effects is just overkill. Maybe programmers would be happy with being able to write an annotation like @pure on their methods and closures, and leave it at that. Enforcing purity would not be too difficult I think (ignoring the well known problem of the termination effect), and be much easier for programmers to reason about.

My wrists have also started acting up again, so I am not entirely sure how to deal with that, yet continue pushing my current research projects forward.  It has been suggested to me to look into voice recognition software, but I am not sure how compatible that would be with my current workflow.  Not to mention that I can only imagine how much it would annoy the people in the adjoining offices given that they have already expressed displeasure at all the beeping caused by emacs on my desktop computer.

Comments (4)