Julia Subtyping - a Rational Reconstruction

on YouTube ↗20m

" summary

Provides a precise formal definition of Julia’s subtype relation plus a reference implementation that logs and replays actual runtime subtype queries, validating behavior against real Julia code. Instrumentation runs 6,014,476 queries and finds 122 mismatches—120 are implementation bugs that get fixed, 2 remain under discussion. The spec encodes existential/forall handling, the two-stack search for normalization, the diagonal constraint for repeated type variables, and surfaces the exact design tradeoffs that explain surprising departures from semantic subtyping.

AI-written summary · about

" chapters (10)

1. 0:00Start
2. 2:51The type of the arguments
3. 3:31Subtyping: intuitions
4. 4:49A precise specification
5. 7:05Subtyping union types
6. 8:00Subtyping parametric types
7. 9:04Union All (aka. Existential Types)
8. 10:24Subtyping Union All
9. 15:10Solving the Union type exist query
10. 16:02Uniqueness of the bottom type