Sound Default-Typed Scheme (Position Paper)

on YouTube ↗20m

" summary

Proposes a concrete default typing system where each expression carries a plausibility-ranked set of types (rank 0 = common, rank ∞ = impossible), implemented as a Racket macro layer that emits SMT-style constraints and performs lexicographic minimization to pick the weakest plausible rank. Prototype generates efficient code with no runtime checks when defaults hold, and emits concrete counterexamples (via a D3-backed trace) when rank-0 assumptions fail. Current prototype works intra-module and for first-order code; module boundaries and higher-order cases remain unsupported.

AI-written summary · about

" chapters (10)

1. 0:00Default-typed Scheme intro
2. 1:04Latency load balancer example
3. 3:55Typing trade-offs and goals
4. 5:20Rank types explained
5. 7:03Policy table and typing rules
6. 9:36Gradual probability and refinement
7. 11:42Constraint solving and errors
8. 13:52Compilation and limitations
9. 15:19Next steps and future
10. 16:03Q&A