Answer type polymorphism in call-by-name continuation passing

Abstract. This paper studies continuations by means of a polymorphic type system. The traditional call-by-name continuation passing style transform admits a typing in which some answer types are polymorphic, even in the presence of first-class control operators. By building on this polymorphic typing, and using parametricity reasoning, we show that the call-by-name transform satisfies the eta-law, and is in fact isomorphic to the more recent CPS transform defined by Streicher.