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 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.