Type Narrowing the Hard Way
summary
A litmus-suite called the if t benchmark runs on eight real typecheckers and shows everyone handles basic narrowing but disagree widely on harder cases; set-theoretic types give a neat declarative spec (slow or tricky for singletons like “even”), while the pragmatic common approach is a syntactic meta-function tacked onto if rules. The implemented occurrence typing (Typed Racket, Typed Clojure) is compositional and catches lying predicates but complicates the checker and produces hard-to-read errors; a property-based generator is under development to find predicate unsoundness.
AI-written summary · about
chapters (11)
- 0:00Type narrowing introduction
- 1:04Why type narrowing matters
- 3:08Basic narrowing examples
- 4:32Higher-order narrowing with filter
- 5:54Introducing ift benchmark
- 8:19Easy narrowing implementation
- 11:50Beautiful narrowing with set types
- 16:20Hard way with occurrence typing
- 19:48Occurrence typing challenges
- 20:30Testing predicates with PBT
- 21:13Q&A
related talks
46mThe Calculated Typer (Functional Pearl)
19mIll-Typed Programs Don't Evaluate
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
23mTowards a Performance Comparison of Syntax and Type-Directed NbE
30mDotty and types: the story so far
30mConstraint Typing with Boolean Algebra
56mOn Type-Based Techniques for Program Manipulation
29mType Checking with Rewriting Rules