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.
