On Wednesday, we finally finished revisions to the TOPLAS version of AspectML: A Polymorphic Aspect-oriented Functional Programming Language. While somewhat tedious, I think the revisions made the paper more approachable. Not to mention fixing a number of typos, omissions, and minor bugs. Assuming the reviewers dont' request another round of revisions, this will hopefully be about the last time I need to touch this paper.

Also, in conjunction with finishing these revisions, we made an α-quality release of the AspectML interpreter that corresponds to the language as described in the paper. It doesn't really come with any real documentation, but if you're interested in trying it and can't figure it out, let me know. You should only really need to have a recent version of SML/NJ handy. However, I highly recommend using rlwrap if you aren't running SML from emacs or some such.

One thing about WordPress that has been annoying me for quite some time is that it mangles UTF-8 in the subject of e-mail messages it sends out. Consequently, because my site uses the &exists; character, the subject line of messages I get about it are garbage. Apparently this has been a bug in WordPress for quite some time, but I did find that there is a plugin that will fix the problem. Of course I'll need to wait for someone to comment or what not before I'll know whether it truly works.

Also somewhat strange was the other day I received a spam comment after having installed WordPress Hash Cash. This leads me to believe that it is either broken or there are actually people out there spamming from an actual web browser. I suppose in theory it wouldn't be out of the question to robotize a web browser. The arms race continues. I still haven't come up with an effective way of filtering image-based spam. Though I sometimes suspect that some of it gets through because one of my spam filters fails to run if it somehow failed to acquire a lock.

Is it possible to compute a regular expression over byte sequences to match against specific ranges of Unicode glyphs encoded using UTF-8? This comes up when you're stuck using lexer generators that only understand byte sequences.

I have to assume that it must be possible, becaue at worst you can just union together the UTF-8 byte sequences for every glyph in the range. However, given how large some ranges can be, this would probably be very inefficient. The better question is whether or not there is a smarter way of constructing your regular-expression or DFA. Though right now I'm not inclined to think about it too deeply as I know if it really comes down to doing this, I can just do it the blindingly stupid way and write some DFA minimization code.

Though maybe this is just a "Photoshop" job.

Over the past few weeks I've been starting to feel that perhaps it was time to reconsider my choice of editors again. There are many things to like about vim, but it seems like an evolutionary dead-end. The basics are simple, but the overall design doesn't seem very unified. I did a little programming in vim's "internal" language, although you have the option to link vim against a number of other languages, and it seemed quite clusmy. Not to mention quite imperative. Plus, many projects I work on, like AspectML/InforML are written in languages that do not currently have adequate support in vim. Alan may be a little disappointed with me, but I gather he is using TextMate for most things these days anyway.

So I have been considering my option. I did look at TextMate, as Alan had mentioned it, but it didn't seem too compelling to me. To me it seems somewhat like a reimplementation of emacs, without the Lisp. Not to say that wouldn't be a good thing, but it was also entirely MacOS X specific. I'm a very cross-platform fellow, so I need something that works essentially everywhere.

Next I took a look at jEdit. It seemed fairly nice, and had some interesting plugins. Unfortunately, it was just far too slow on my laptop for regular use. So I looked around a bit more, but I hadn't really found anything that seemed promising. Then on Friday, during a discussion with some of the PLClub folks, the question of antialiased fonts in emacs came up. (X)emacs support for antialiased text was one reason I decided to switch to vim; the other was vim's superior support for UTF-8.

Currently, the "release" version of emacs, 21.x, still lacks both. But the "emacs-unicode-2" branch in CVS does have them. However, I gather that this branch is intended to become emacs 23.x, which either implies they plan of skipping version 22.x altogether, or at the current release rate it will be more than a few years before it is released. Still, I checked it out of CVS and was able to build it without too much trouble. Despite having a stern warning about it begin "alpha quality" on the start up blurb, so far it has been pretty stable for my needs.

So I'm back to emacs again after a number of years. I still think there is a need for a new cross platform editor. I did find Eclipse quite promising, but I think it currently suffers from being perceived as just for editing Java and a seemingly steep learning curve when it comes to developing new editing modes (at least I couldn't find any tutorials or documentation).

It has been far too long since I've sat down and written something for ∃xistential Type. Somehow there never seems to quite enough time. Perhaps it is because I've been accumulating a pretty significant backlog. Some of the lecturing I have been doing has been a contributing factor. I gave a presentation on Erlang a couple weeks ago for the Systems Seminar, and last week (and tomorrow) I have been presenting a paper on dependently typed proof assistants for CIS700.

One interesting thing that came up the other day was that Stephanie pointed me to a newish paper called Statically Verified Type-Preserving Code Transformations in Haskell" by Guillemette and Monnier which was essentially about taking the ideas we developed in "Boxes Go Bananas" (BGB) and extending them for the internals of a simple compiler that is statically verified by use of GADT constraints. It was heartening to see that the paper continues to have life left in it.

It also inspired me to examine more closely whether the ideas could be applied with in Coq. The short answer: Yes, you can implement our encoding on higher-order abstract syntax in Coq. However, by implement, that means you can construct data-structures with function spaces and have a catamorphism operator over them with the type described in BGB. However, this is not enough as the basic catamorphism is not expressive enough to truly be a useful induction principle. Therefore, I am continuing to work on showing that an appropriately expressive induction principle can also be constructed. I have made some progress in this direction, but I am having a difficult time proving a few things that I feel ought to be pretty easy.

Finally, while still on the topic of BGB, the "final" version for the Journal of Functional Programming has been submitted. I don't know if it has been scheduled for a particular volume or issue yet.

I've started following along with Frank's course on logic programming via the online course notes. Maybe it is just because I've taken so many classes with him, but I find his notes much more approachable and comprehensive than other materials on logic programming I've tried reading. Anyway, I highly recommend them if you would like to know more about how logic programming languages work.