Type-Checking Heterogeneous Sequences in a Simple Embeddable Type System
summary
Claims a practical method to type-check heterogeneously typed sequences by inventing rational type expressions and compiling them to symbolic finite automata that match sequences in linear time. Key technical tool is maximal disjoint type decomposition that partitions overlapping/subtyping types so derivatives are computable even when subtype decidability is unknown. Implementation exists in Common Lisp, Clojure, Scala, Python, produces correct deterministic automata (sometimes with useless states) and reduces a worst-case 32-partition blowup to 10 in the example.
AI-written summary · about
chapters (12)
- 0:00Type checking sequences
- 1:06Project history
- 2:11Regular type expressions
- 3:38Type lattice challenges
- 5:45Finite automaton for sequences
- 7:56Key type system challenges
- 10:22Type lattices across languages
- 13:17Brovsky derivative
- 17:57Maximal disjoint decomposition
- 21:12Finite automaton correctness
- 23:42Conclusion
- 24:44Q&A
related talks
30mRecognizing regular patterns in mixed type sequences using Symbolic Finite Automata
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
46mThe Calculated Typer (Functional Pearl)
21mPolymorphic Type Inference for Dynamic Languages
56mOn Type-Based Techniques for Program Manipulation
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
17mFrom Traces to Program Incorrectness: A Type-Theoretic Approach
14mType-Sensitive Algebraic Macros