The formal connections between the static information hiding mechanism of parametric polymorphism and the dynamic mechanism of sealing was first studied by Sumii and Pierce in 2000. While several significant and interesting results about these connections were obtained over the years, Sumii and Pierce’s conjecture that there exists a fully abstract compilation from parametric polymorphism to sealing is still open after more than 15 years.

In this talk, we will explain that their conjecture is false by providing examples of terms whose compilation is not fully-abstract. We identify the problem that causes the failure of full-abstraction in the way in which quantified type variables can be instantiated with each other. We then develop a fully-abstract compilation from a meaningful subset of \sysfname with polymorphism but with a restricted syntax of types to a standard untyped lambda-calculus with sealing. This compiler not only shows that the parametricity properties of \sysfname are preserved, it also shows that the use of dynamic sealing by the compiler does not leak any information to target language contexts – a remarkable property since creation of seals is a side effect in the target language while the source language is side effect-free.

While the counterexample and full abstraction theorem and the main result of this paper, we also believe that the proof techniques we use have independent interest, and may find other applications, for instance for the development of gradual type systems for languages with parametric polymorphism.