Explicit Polymorphism and CPS Conversion,
Abstract
We study the typing properties of CPS conversion for an extension of F omega, with control operators. Two classes of evaluation strategies are considered, each with call-by-name and call-by-value variants. Under the 'standard' strategies, constructor abstractions are values, and constructor applications can lead to non-trivial control effects. In contrast, the 'ML-like' strategies evaluate beneath constructor abstractions, reflecting the usual interpretation of programs in languages based on implicit polymorphism. Three continuation passing style sub-languages are considered, one on which the standard strategies coincide, one on which the ML-like strategies coincide, and one on which all the strategies coincide. Compositional, type-preserving CPS transformation algorithms are given for the standard strategies, resulting in terms on which all evaluation strategies coincide. This has as a corollary the soundness and termination of well-typed programs under the standard evaluation strategies. A similar result is obtained for the ML-like call-by-name strategy. In contrast, such results are obtained for the call-by value ML-like strategy only for a restricted sub-language in which constructor abstractions are limited to values.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1992
- Accession Number
- ADA258635
Entities
People
- Mark Lillibridge
- Robert Harper
Organizations
- Carnegie Mellon University