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.

6 Comments »

  1. Andrew said,

    December 15, 2007 @ 8:02 pm

    Check the recent Coq club archives. There was a huge discussion about the issue of inductive definitions with lists of the thing you are defining in them, and all the ways you can deal with it. I think Benjamin Pierce asked the first question. I think the best solution was presented was to come up with your own induction hypothesis that correctly works on the list. So there is slightly more work per-definition, but then everything is nice.

  2. washburn said,

    December 15, 2007 @ 8:05 pm

    Right, but following that discussion, the people thinking very hard about this at Penn seemed to conclude what I describe above, along with using coercions, is the best thing to be doing. I am not very clear on why this supposed to be better than proving a custom induction principle.

  3. Andrew said,

    December 16, 2007 @ 1:51 am

    I find that pretty surprising.

  4. Brian said,

    December 16, 2007 @ 3:13 am

    If you read the discussion on coq-club that Pierce started, you’ll notice that no one actually proves a principle that lets you conclude that you’ve proved some property P about all Xs and some property P’ about all lists of Xs—you only get the bit involving P. It’s straightforward to get the P’ bit as well, but done naively, there is a lot of code duplication. Moreover, you’d have to play similar games for any function that needed to be defined over that datatype.

    I think the trick is to do something like what Yves Bertot suggests at the end of this (non-)bug report: http://logical.futurs.inria.fr/cgi-bin/bugzilla/show_bug.cgi?id=1751

  5. Andrew said,

    December 16, 2007 @ 5:26 am

    Ah, I see. Yeah, that is an annoying series of things. I guess I’ve never had to deal with that combination of things.

  6. ∃xistential Type » Retraction on Coq and lists said,

    December 18, 2007 @ 10:43 am

    […] so everything I said the other day about mutually defining your ASTs in Coq with custom lists, and then using Coq’s implicit […]

RSS feed for comments on this post · TrackBack URI

Leave a Comment