Decidable Subtyping of Existential Types for Julia

on YouTube ↗19m

" summary

Proves Julia’s runtime subtyping is undecidable via reduction from System F<: and designs a restricted grammar that is stratify types into method signatures and value types (top-level existentials plus use-site-variance in values) with an algorithmic decision procedure for that fragment. Performs corpus analysis over ~9,000 packages (≈16.5M LOC, ~2.2M extracted annotations) and finds only four types that violate the restriction. No compiler replacement is delivered; paper gives formal proofs and an algorithm.

AI-written summary · about

" chapters (11)

1. 0:00Introduction
2. 1:44Undecidability in Julia subtype
3. 3:06Restricting Julia's type language
4. 4:53Existential types challenges
5. 7:00Impredicative existentials proof
6. 9:30Stratifying Julia types
7. 11:37Decision procedure
8. 13:48Constraint resolution
9. 15:35Evaluating real-world code
10. 16:58Summary of results
11. 17:22Q&A