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.

@article{IgarashiOST24,
  title = {Space-Efficient Polymorphic Gradual Typing, Mostly Parametric},
  author = {Atsushi Igarashi and Shota Ozaki and Taro Sekiyama and Yudai Tanabe},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {PLDI},
  year = {2024},
  doi = {10.1145/3656441}
}