AspectML came up in a discussion on aspects over at Lambda the Ultimate.

Also, this morning the Journal of Functional Programming accepted our extended version of "Boxes Go Bananas" as ready for publication.  Just need to track down any last typos...

I've been thinking about trying to do my dissertation in ConTeXt rather than LaTeX.  There seems to be quite a bit of nice stuff that can be done easily in ConTeXt. This might be the kind of thing to try over winter break, but I do kind of wonder whether the benefits would be too small to justify it. With a little more work, the definitions I used for my proposal will probably work well enough.

In other news, Karl Crary never responded to my inquiries concerning when a public snapshot might become available, so I'm inclined to just forge ahead on my own efforts.  I need to find some time to sit down and rewrite OCamlTeX to take advantage of the forthcoming extensions that are part of LuaTeX.

One thing I've been thinking about a bit lately is whether it might be possible to smooth over quite a number of the problems with Twelf via essentially providing an additional meta-language. For example, something like a Haskell library that can interface with the Twelf server. It would be possible to essentially use the library to do things the way they are done now, but also use something like the parametricity trick from "Boxes Go Bananas" to programmatically construct some bits of proofs. I guess I'm kind of thinking of Delphin lite perhaps. But then it would be possible to write combinators for giving you "generic" sums and products and false elimination.

The primary problem is that while it would be possible to enforce that HOAS is used correctly, it would be difficult to ensure that only well-typed LF terms are manipulated. The other serious problem is that it would require building a considerable amount on intelligence into the system to be able to provide comprehensible error messages. As it is Twelf doesn't always provide particularly enlightening error messages, so it would perhaps even require adding heuristics to interrogate the twelf-server for additional information that most users don't know to consult.

However, perhaps after I've had more time to work with Coq this semester, I'll conclude that such effort is pointless.  Adam Chlipala was pushing programming entirely in Coq while I was at ICFP.  It is something I've certainly considered before, but I don't think I have any projects at the moment where I can really justify the learning curve for doing so.

Recently I became aware of a 2005 Intel white paper on ray tracing. It is intriguing mostly because, aside from some demoscene hacks, the impression I've gotten is that ray tracing has been far too computationally expensive for real-time rendering. Quoting somewhat selectively from Chapter 13 ("The Future") of Real-Time Rendering by Möller and Haines

Some argue that in the very long term, rendering may best be solved by some variant of ray tracing, in which huge numbers of rays sample the environment for the eye's view of each frame. And there will also be colonies on Mars, underwater cities, and personal jet packs.

However, on the preceding page they do say

For whatever reasons [...], Moore's Law is currently being beaten in this areaThis situation seems unlikely to continue, and the application-stage processors are still following Moore's Law, but it is an interesting phenomenon. At a six-month doubling rate, an average frame of ABL [A Bug's Life] would be possible at real-time rates by 2007. We can always dream...

The book was published in 1999, but 2007 isn't far off.

In any event, the white paper claims that it isn't just increasing computational power that is making ray tracing viable. They argue, without much in the way of supporting mathematics, that for a fixed resolution as scene complexity increases, ray tracing scales logarithmically. Whereas raster techniques, presumably, scale linearly. I couldn't find a clear mention in the article of their conjectured scaling for raster techniques, but looking at their log-plot performance curves, I would surmise that it is at least a low polynomial.

Their experiments essentially supported this, that for sufficiently complex scenes a multithreaded software ray tracer running on a multicore processor would out perform a hardware raster renderer.

It makes me want to sit down an write a nice ray-tracer.

Unlike Philadelphia or Denver, PDX is civilized enough to provide free wireless.

Anyway, I'm on my way back to Philadelphia. I'm really looking forward to returning to research; I've been rapidly accumulating interesting things I want to try, investigate, and read. While ICFP and etc. was fun, it has been very tiring. I definitely have a very cool advisor.

Also, I did spend a few minutes trying to get my colored pretty printing support for GHC working.  I kind of succeeded.  I could actually produce colors, but due to the way the Hughes-Peyton Jones pretty printer wants certain things to commute, I could come up with a good way to prevent parts of the accumulated document from getting pushed inside of color blocks that they shouldn't.

So I'm going to read through the paper when I get back to Philly and hopefully figure out a way to integrate "rich text" into Hughes-Peyton Jones pretty printing.

Wireless access wasn't as easily available yesterday. Initially they chose to assign the hub a key that was actually longer than should be valid, which confused some wireless drivers considerably (Windows XP refused to acknowledge keys that are the incorrect length or format).

Stephanie's presentation went very well I think. It will be interesting to see whether any of RepLib will be adopted as part of the "standard" generic library for Haskell that Johan Jeuring has proposed. I spent part of the afternoon sitting in on an informal Standard ML evolution meeting. There was not as much emphasis on the process as I had really hoped. After I had to bail I gather a few things were decided at least.

Late last evening I had an idea about how to deal with labeling abstract syntax trees using SML exn's.  There really needs to be a way to create them that doesn't call them "exceptions".

I've been talking with so many people that it is really hard to say anything concrete about that.

I can slip in a little bit about typography even, as I finally saw a demo of Karl Crary's mTeX.  I need to remember to ask Karl about how long it might be before others can start testing it.  I'm not sure how much sense it makes to devote to the future of OCamlTeX and such if mTeX will fill that niche well enough.  In other news, while chatting with Tom7 and some other CMU folks, Tom gave his approval of my ambitions to work on better math fonts.  I'll get back to it really soon now, I promise.

Okay, I should probably start paying attention to Dave's talk.

I survived my presentation at WGP, which seemed to go over well.  I felt that I was working through it quite quickly, but Stephanie thought that it wasn't too bad except at the very beginning.

Now I get to work on having fun and doing some networking.  There is some kind of Galois dinner that I'll be attending Monday evening.

I should stop writing and pay attention to the talk now.

We're nearing the half-way point of day two of the GHC hackathon.  First SimonPJ gave a run through what "factorial" looks like through various stages of the compiler.  Then SimonM gave us a tutorial on tracking down space leaks.  SimonPJ is now explaining GHC as an API.

This afternoon it looks like I am going to work on improving the quality of pretty-printing for the Core language, as well as perhaps reviving "ExternalCore" which can be used if you want to write another front-end targeting the Core language.

Air travel is unsurprisingly as miserable as ever.  But Portland is beautiful.

At the GHC Hackathon at the moment. Quite jet-lagged. I'll write more soonish.