Survey Workshop on Typeful Compilation
September 29, 2000
ROPAS, KAIST
Program Organizer: Oukseh Lee
Explicit polymorphism and CPS conversion.
Robert Harper, Mark Lillibridge.
ACM Symposium on Principles of Programming Languages, pages 206-219, January 1993.
(Presented by Jungtaek Kim)
Abstract
We study the typing properties of CPS conversion for an extension of F 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 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-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.
Discussion
the key idea is that CPS transformation is possible with types.
need to restrict the type system in order to type-check callcc or throw.
some use CPS but some don't. it is necessary for compiling callcc or throw because they are hard to implement without CPS.
we are skeptical because CPS is hard to understand and to debug.
nML will not support CPS.
however, CPS is a good theoretical tool for reasoning some language features.
A-normal form is an alternative. (name all intermediate computed value)
Typed Closure Conversion.
Yosuhiko Minamide, Greg Morrisett, Robert Harper.
ACM Symposium on Principles of Programming Languages, pages 271-283, January 1996.
(Presented by Kwangkeun Yi)
Abstract
Discussion
the key point is "type-preserving".
even though type does not help closure conversion,
without type passing in closure conversion step,
low-level type-based optimization
is impossible.
what's the difference from \lambda-lifting?
it is possible without existential type?
it is important to make less closure.
Oukseh Lee