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.


  1. Chris said,

    January 14, 2008 @ 11:02 pm

    Regarding RSI, I don’t know anything about your experiences and trials so far, but the Kinesis contoured keyboards (Dvorak mode) have helped me tremendously. I have one at home, one at work, and one older one in the closet for emergencies. Not cheap, but comfortable.

    One day I also undertook a radical remapping of Emacs key bindings.. not sure I ever wrote about that publicly, but I could make my efforts available if anyone wants. The rationale was that on Kinesis (and laptop keyboards), the arrow keys, home/end, and page up/down are not a huge reach from home position (as they are on standard 102-key PC). Therefore, it’s not necessary to continue using C-p, C-n, C-f, C-b, C-a, C-e, C-v, M-v, etc., etc. Therefore, they can be remapped to other things, leading to less severe chording. Example: exchange-point-and-mark is now just C-p, switch-buffer is just C-b, and whole maps of related commands sit on mnemonic keys like M-v for version control stuff, M-b for buffer commands, M-4 for window commands, M-5 for frame commands, etc.

    Non-programmers seem to think voice recognition is the answer, but I agree that I’m extremely skeptical. If your workflow can be reduced essentially to dictation, then maybe it’s fine. But for programming, TeX, non-trivial editing, command lines, and controlling complex applications.. I just can’t imagine it will work.

  2. washburn said,

    January 14, 2008 @ 11:09 pm

    @Chris: Just a quick comment, it is about bedtime here so I’ll say more later, it was actually a tenured professor doing PL research at an Ivy league university (not Penn) who recommended voice recognition software, because that is what he uses quite a bit to combat his RSI issues. I will not attempt to speculate on how much programming he truly does anymore, but he does at least do a little LaTeX. I think he may have some fairly complex voice macros.

  3. washburn said,

    January 15, 2008 @ 11:34 am

    @ Chris: I had briefly borrowed a Kinesis keyboard a few years ago, but I think I was also giving Dvorak a try at the same time and I had to give it up after a day or two because I just couldn’t afford to be that unproductive at the time. Another concern of mine is whether relying on a non-standard keyboard would be problematic while I am traveling. Or do you find that as long as you use the Kinesis while at work or at home, you’re fine using a laptop keyboard while you a traveling?

  4. Chris said,

    January 15, 2008 @ 5:16 pm

    Yes, I switched to Dvorak long ago, while still an undergrad (~1994) and before any RSI. That took some time. But from there, the switch to Kinesis was easy.

    When I first injured myself (1999), I swore I’d never touch a laptop keyboard again, and promptly sold my nearly-new Toshiba. Over the years I softened on this (and learned more about my limitations), and now I use laptop keyboards pretty regularly. If I have really intense long-term hacking or writing to do, I’ll definitely use the Kinesis, but that’s generally not the case when traveling.

    Among my other tricks (regardless of keyboard) are break timers (AntiRSI on Mac) and sticky modifier keys (allows me to be a little lazy/sloppy about chords).

RSS feed for comments on this post · TrackBack URI

Leave a Comment