Polymorphic type assignment and CPS conversion

Meyer and Wand established that the type of a term in the simply typed -calculus may be related in a straightforward manner to the type of its call-by-value CPS transform. This typing property may be extended to Scheme-like continuation-passing primitives, from which the soundness of these extensions follows. We study the extension of these results to the Damas-Milner polymorphic type assignment system under both the call-by-value and call-by-name interpretations. We obtain CPS transforms for the call-by-value interpretation, provided that the polymorphic let is restricted to values. and for the call-by-name interpretation with no restrictions. We prove that there is no call-by-value CPS transform for the full Damas-Milner language that validates the Meyer-Wand typing property and is equivalent to the standard call-by-value transform up to operational equivalence.This is a revised version of a paper presented at the ACM SIGPLAN Workshop on Continuations, San Francisco, June 1992.This work was sponsored by the Defense Advanced Research Projects Agency, CSTO, under the title The Fox Project: Advanced Development of Systems Software, ARPA Order No. 8313, issued by ESD/AVS under Contract No. F19628-91-C-0168. Supported by a National Science Foundation Graduate Fellowship.