Relational Parametricity for Control Considered as a Computational Effect

This paper investigates parametric polymorphism in the presence of control operators. Our approach is to specialise a general type theory combining polymorphism and computational effects, by extending it with additional constants expressing control. By defining relationally parametric models of this extended calculus, we capture the interaction between parametricity and control. As a worked example, we show that recent results of M. Hasegawa on type definability in the second-order (call-by-name) λμ-calculus arise as special cases of general results valid for arbitrary computational effects.