Archive for research

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)


There is a current thread on Lambda the Ultimate at the moment on predictions for 2008. I will have to remember to look at it again later this year.

Most of the predictions concerning Scala are positive.

I would have to agree with Sean that there have been many years I've heard that concurrency will be the big thing, but I do not feel there has been too many big developments in the area recently. Robin Milner has recently released a draft book on his theory of bigraphs, his newer generic model for concurrency. There is actually an even newer draft of the book, but that is not presently linked from his website, so I am not sure whether I should publish the link.


Retraction on Coq and lists

Okay, so everything I said the other day about mutually defining your ASTs in Coq with custom lists, and then using Coq's implicit coercions to move back and forth between lists as defined in Coq's standard library, does not work.  Firstly, the coercions will not always be inserted when you will need them, and even inserting the coercions manually does not work out well as Coq will then not be able to determine that recursive functions you define on your ASTs will necessarily terminate.

So I have switched back to using lists from the standard library and hoping that defining custom induction principles based upon Yves Bertot's suggestion in the discussion here will work for everything I need to do.

Comments (2)


I gave a mild promise of more programming languages related material after depositing my dissertation, but so far I have not really come through on that.  I am not sure how much I will cover in this particular posting, but we'll see.

Firstly, I am have been merging material on generalized parametricity that I revised and expanded, as part of my dissertation, back into a journal version of my LICS 2005 paper.  My plan current plan is to submit it to LMCS.

I have just barely started on creating a Coq formalization of Featherweight Scala. It is something that could probably done in Twelf, but I am trying to believe that Coq is more modular at the moment. However, I am currently feeling somewhat disillusioned because I am told that defining part of an AST like the following

Inductive exp : Set :=
| exp_tuple : list exp -> exp

where list is the list data type that is part of Coq basis library, will not allow one to prove the sorts of theorems one would like. Instead, I am told I should write a mutually inductive AST, something like the following

Inductive exp : Set :=
| exp_tuple : exp_list -> exp
with exp_list : Set :=
| exp_list_nil : exp_list
| exp_list_cons : exp -> exp_list -> exp_list.

Doing things this way almost negates the benefits one would assume you get from having polymorphism in Coq. Now I am told for the latter definition it is possible to make clever use of Coq's coercions to convert exp_lists back and forth between lists, but I'll have to see how well this works for Featherweight Scala. Maybe, maybe Delphin will be usable someday.

My main project so far other than getting settled in, dealing with Swiss bureaucracy, and preparing a talk on generalized parametricity for the Tresor seminar, has been to start thinking about and to soon start implementing virtual classes for Scala. Virtual classes are kind of strange things, I did not really understand them until I started working on the problem here at EPFL. The idea is basically that you define some »module« class

class A {
  class Inner <: { val x : Int = 42 }

with an inner class, and then you may inherit from the module class and override the inner class. The idea is for that to look something like the following in Scala

class B extends {
  class Inner <: { val y : Int = -42 }

Here B.Inner has both a member x and a member y. Things become more interesting when you include inheritance from the inner class

class A {
  class Inner <: { val x : Int = 42 }
  class Innie extends Inner { val z : Int = 0 }
class B extends {
  class Inner <: { val y : Int = -42 }

Now B.Innie also has a member y because we have overridden its parent class. The idea is that for Scala, this kind of behavior can just be treated as complex syntactic sugar for abstract type members and trait composition. However, it is getting late here, so I'll talk more about that some other time.

Comments (6)

Absolutely done

I am finally absolutely and completely done with my doctorate. There is no doubt that I am now Doctor Washburn. On Tuesday, I deposited my dissertation, which proved to be more of an adventure than I expected.

For reasons I have not bothered investigating, LaTeX numbered the third page in the document as "ii" when it should have been "iii" (the first two pages are unnumbered).  However, this was the only mistake in terms of formatting that the ruler-lady noticed, so I only needed to reprint the pages numbered using lowercase Roman numerals.  She even offered up some of her spare sheets of the required 100% cotton, 20lb (or greater), acid free paper so that I could reprint the needed pages.  However, upon returning to Levine Hall to make the correction (\setcounter{page}{3} on the dedication page) and reprinting, I determined that we must have made an off-by-one error and the ruler-lady had given me one too few sheets.  So then I dashed off to the Penn Bookstore to purchase some more 100% cotton, etc. paper.  But I was able to get it all fixed and was even able to deposit the corrected pages without making a new appointment.

As far as double spacing goes, I went with a \baselinestretch of 1.5 as one of my colleagues said that he did so and it worked for him.  In practice, the ruler-lady did not actually ever lift her ruler from the table – not even to check the margins. She did ask me what size typeface I was using and whether my abstract was double spaced.

I have put a copy of the document that I deposited online.  I'm almost certain that the careful reader will find arbitrarily many typos, but I am also certain that I could expend an arbitrary amount of effort making it a better document and the returns were already diminishing. Still, if you do find any mistakes, please e-mail me so that I can fix them before I print up copies of the "director's cut" version via Lulu.

I am hoping that I will now have a little more time to write here on ∃xistential Type. I have a few non-typography related things that I will probably write up soon, for those of you bored by my endless tweaking of Gentzen Symbol.

Comments (11)


I've successfully defended my dissertation.  My committee would like some revisions to the way I motivate a few things in my introductory chapter, but that should definitely be possible before I leave the country.

I could really use a nap.

Comments (7)

Defense against the dark arts

This Thursday at 9AM  I will defend my thesis against my committee, and anyone else that shows up and attempts to ask me difficult questions. But really, who would want to get up that early to do that?

Assuming that I can successfully disarm two assistant and two full professors,  I will be all set to start working on Scala related things at EPFL.  Of course, I've bought a plane ticket to Geneva, Switzerland for the 26th, so unless my rhetorical-fu is truly mediocre, that will be happening one way or another.

Comments (3)

Curation woes

I would like to know if M. O. van Leer has a first name and perhaps even exists. As far as I can tell he was a co-author on a FPCA paper on Clean in 1987, has not published anything since, and is not listed as a former member of the Software Technology Research Group in Nijmegen.


Step one complete, and an upgrade

I've finally handed off a draft of my dissertation to my committee. I hope that I will find time to update more frequently from here on out.

In other news, I've finally taken this opportunity to upgrade to the latest version of WordPress in the hopes that it will prevent the spread of that malignant blogroll spam that you may have been noticing. I guess this is what happens when you run software written in PHP. Maybe I will have time to think about a custom theme before too long as well.

Comments (4)

I come bearing links

While I have been in hiding, toiling on my dissertation, a rather large number of links have been accumulating in my to-do list. I'll hopefully write more on the status of my dissertation soon.


A few weeks ago I became frustrated with the capabilities of FontBook on Mac OS X and Gnome Specimen and gucharmap under X11. I spent some time searching and came across Linotype's FontExplorer X. My best description of it would be iTunes for fonts. Not only does it let you manage, examine, and compare the fonts you do have, it lets your preview and purchase fonts from Linotype.

I also came across the UnicodeChecker application (again MacOS X only) which perhaps provides a more detailed examination and exploration of the properties of Unicode glyphs.


I'm not sure where I read about it, but I recently came across, "The Online Encyclopedia of Western Signs and Ideograms". I haven't needed to consult it yet, but it is fairly interesting just to see what it gives you when asking for a random sign.

I've known about this for a while, but didn't think to mention it until now: the entirety of the Fifteenth edition of the Chicago Manual of Style can be found online. Useful when you don't want to carry around the hardcopy, and searchable. Unfortunately, looking at it again now, the fact that it says in the corner »University of Pennsylvania« makes me believe that is this probably not a free service. And indeed, I just verified this with my desktop, which does not have a cached cookie from inside the Penn network.


From Lambda the Ultimate, I learned about a paper giving a functional description of the »galleys« layout algorithm used by the lout document processing system.

This also reminded me of the earlier post, also by Neel, on a functional description of TeX's formula layout algorithm.

I also went looking and Kingston has a nice paper on the design of lout, and website on the eventual successor to lout, Nonpareil. lout is an interesting system, though for some reason when I first encountered it many years ago I didn't seem to think it produced as nice of output as TeX. I haven't tried to reevaluate this at the moment, and see whether it has changed or I was simply wrong in the first place.

Also, something else on Lambda the Ultimate led to me to discover the Juno-2 structured drawing editor. I've only had a chance to read about it briefly, but it sounds quite a bit like what I have envisioned for the font editor I've been thinking about for a while, but haven't found the time to seriously start yet.

Finally, while writing this section, I came across another Lambda the Ultimate post on Skribe, a Scheme based document formatting system. It however it seems to be more of a macro layer on top on HTML and LaTeX, rather than a fully integrated system.

Comments (2)

« Previous Page« Previous entries « Previous Page · Next Page » Next entries »Next Page »