Structural Subtyping as Parametric Polymorphism

on YouTube ↗17m

" summary

Compares structural subtyping for records and variants with row and presence polymorphism and gives compositional translations that preserve types and operational behaviour for several restricted cases, plus formal proofs of impossibility: full subtyping cannot be encoded by polymorphism, and there is no type-only, compositional translation from simple record subtyping to presence polymorphism or from simple variant subtyping to row polymorphism. Shows common upcasts admit local encodings via coercion (destruct/reconstruct) or via type abstraction and instantiation but requires higher-rank polymorphism except under type-inference and rank restrictions.

AI-written summary · about

" chapters (13)

1. 0:00Structural subtyping intro
2. 2:07Lambda calculus with variants/records
3. 3:33Extending calculus with subtyping
4. 4:37Parametric polymorphism for variants/records
5. 6:02Variants/records subtyping duality
6. 7:53Presence polymorphism for records
7. 9:57Rank-2 translations negative results
8. 11:23Rank-1 polymorphism for subtyping
9. 12:46Formal proofs and meta-theory
10. 13:51Takeaways and limitations
11. 14:12Q&A: Subtyping in practice
12. 15:15Q&A: Compositionality in typing
13. 16:21Q&A: Nominal vs structural