Archive for December, 2007

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)

Type Generator

Last weekend, I stopped into mudac, the museum for design here in Lausanne, for a few hours. The primary reason for the visit is that another postdoc here at EPFL, Ingmar, had told me that that as part of an exhibit on the 2007 recipients of Swiss Federal Design Grant there was a program on display that let you play with a the parameters of a typeface.

An installation on meta-type designMore of the installationA video component to the installation.My attempt to make some legible
A close up of one of the figuresAnother close upAnd another closeup

It was interesting, but I would have to say that I was impressed. The software Type Generator was designed by Remo Caminada and Ludovic Varone, and programming in Flash by Patrick Vuarnoz.

I think my impression may been coloured by the fact that the user interface was entirely in German, and therefore it was quite difficult to puzzle out what sliders did which things.  However, I felt that it was very difficult to create a reasonable typeface merely by tweaking the parameters.  I felt that there parameters could have been better constrained to prevent the user from adjusting them in ways that simply exceeded what was sensible.  It very easy to tweak some parameter and suddenly have spikes sprout from all the letters because you had caused some curve to extend in the wrong direction.  It could be argued that having such fine controls give the designer greater freedom, but it feels like the wrong level of abstraction.  I think Knuth's Computer Modern, for example, gives you much more sensible parameters to work with.  The version of Type Generator that was available as a demo was clearly not intended to be a completed production development tool, so perhaps some of these complaints would be resolved as it is polished.

Comments

Research

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)

Trajan is the movie font

I just saw this amusing piece about overuse of the Trajan typeface by the folks who design movie posters on Daring Fireball. I will admit that in addition to Warnock, I did use Trajan on the title side of the presentation I gave on Tuesday.

Comments

Initial version of DejaVu Sans Mono package

I just finished pulling out the various bits of LaTeX and OMake I wrote for using the DejaVu Sans Mono font in my dissertation, as suggested by Brian.  You can grab it using darcs get from http://free-the-mallocs.com/repos/dejavu-sans-mono.

You will need to copy the TrueType files for DejaVu Sans Mono and DejaVu Sans into the directory before running omake. DejaVu Sans is required because I needed to steal a few glyphs from it that are not yet in DejaVu Sans Mono. The other notable omission is that I never needed the oblique version of the typeface, but I can add that with just a little more hacking.

Comments (3)