Transposing F to C#: Expressivity of parametric polymorphism in an object-oriented language

We present a type-preserving translation of System F (the polymorphic lambda calculus) into a forthcoming revision of the C] programming language supporting parameterized classes and polymorphic methods. The forthcoming revision of Java in JDK 1.5 also makes a suitable target. We formalize the translation using a subset of C] similar to Featherweight Java. We prove that the translation is fully type-preserving and that it preserves behaviour via the novel use of an environment-style semantics for System F. We observe that whilst parameterized classes alone are sufficient to encode the parameterized datatypes and let-polymorphism of languages such as ML and Haskell, it is the presence of dynamic dispatch for polymorphic methods that supports the encoding of the “first-class polymorphism” found in System F and recent extensions to ML and Haskell.