Parametric Subtyping for Structural Parametric Polymorphism

on YouTube ↗18m

" summary

Paper proves structural subtyping is undecidable for recursive type constructors and defines parametric subtyping as a decidable fragment that enforces Reynolds-style parametricity on type constructors. Decision procedure has two phases: a forward saturation-based decision procedure that computes admissible parametric rules and a terminating backward construction to build derivations. Works on examples like stacks (pushes/pops), even/odd natural numbers, and serialized binary trees, and an implementation/artifact is available for reuse.

AI-written summary · about

" chapters (11)

1. 0:00Parametric subtyping intro
2. 2:35Recursive type constructors
3. 3:42Key idea behind subtyping
4. 6:14Saturation fails with constructors
5. 8:06Subtyping rules explained
6. 9:10Decision procedure
7. 12:49Serialized binary trees example
8. 13:50Contributions and future work
9. 14:58Q&A: Session types limits
10. 16:17Q&A: Restrictions obstacles
11. 17:25Q&A: Forward phase computation