Premium
Transposing F to C ♯ : expressivity of parametric polymorphism in an object‐oriented language
Author(s) -
Kennedy Andrew,
Syme Don
Publication year - 2004
Publication title -
concurrency and computation: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.309
H-Index - 67
eISSN - 1532-0634
pISSN - 1532-0626
DOI - 10.1002/cpe.801
Subject(s) - haskell , programming language , parameterized complexity , computer science , java , system f , object oriented programming , python (programming language) , translation system , generic programming , functional programming , lambda calculus , algorithm , biology , genetics , in vitro
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. Copyright © 2004 John Wiley & Sons, Ltd.