Guillaume André Fradji Martres
The Dependent Object Type (DOT) calculus was designed to put Scala on a sound basis, but while DOT relies on structural subtyping, Scala is a fundamentally class-based language. This impedance mismatch means that a proof of DOT soundness by itself is not enough to declare a particular subset of the language as sound. While a few examples of Scala snippets have been manually translated into DOT, no systematic compilation scheme has been presented so far. In this report we take advantage of the fact that the Featherweight Generic Java (FGJ) calculus can be seen as a subset of Scala (you just have to squint a little bit!) and present a compilation scheme from cast-less FGJ into DOT as well as a proof that a well-typed cast-less FGJ program compiles down to a well-typed DOT term. Due to limitations in DOT subtyping rules, this requires imposing one limitation on our source program: the type parameters of the base types of a class can never refer back to the class itself (this excludes class C extends B[C] as well as class D extends B[E]; class E extends D). While this result is not especially interesting by itself given that FGJ is already known to be sound, it is a first step towards establishing soundness for larger subsets of Scala like the Pathless Scala calculus, the author plans to pursue this in his thesis (currently under preparation) which will also include the content of this report. It also clearly illustrates limitations in DOT that future work may wish to focus on.
2022
