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.