LISP and Symbolic Computation, 6(3/4)361-380
Polymorphic Type Assignment and CPS ConversionRobert Harper, School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA 15213
Mark Lillibridge, School of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA 15213
|
Abstract: Meyer and Wand established that the type of a term in
the simply typed lambda-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-byname
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. Keywords: polymorphism, continuations |
This article is not available online.
A corrigendum can be downloaded [here] or locally [here].
![[picture of journal cover]](../LISP.JPG)