Space-Efficient Polymorphic Gradual Typing, Mostly Parametric

Since the arrival of gradual typing, which allows partially typed code in a single program, efficient implementations of gradual typing have been an active research topic. In this paper, we study the space-efficient problem of gradual typing in the presence of parametric polymorphism. Based on the existing work that showed the impossibility of a space-efficient implementation that supports fully parametric polymorphism, this paper will show that a space-efficient implementation is, in principle, possible by slightly relaxing parametricity. We first develop λC m p ∀ , which is a coercion calculus with mostly parametric polymorphism, and show its relaxed parametricity. Then, we present λS m p ∀ , a space-efficient version of λC m p ∀ , and prove that λS m p ∀ programs can be executed in a space-efficient manner and that translation from λC m p ∀ to λS m p ∀ is type-and semantics-preserving.