Logically Qualified Types for Scala 3
summary
Prototype adds compiler-integrated refinement types to Scala 3, letting types carry boolean predicates that the compiler checks. Implementation uses a lightweight, internal solver based on E-Graph normalization solver, constant folding, unfolding of local vals and congruence to prove implications, so zip/concat length equalities typecheck statically while mismatched cases fail at compile time. Predicates forbid mutable refs and non-case-class equality; runtime-checked casts and pattern-match narrowing bridge static gaps.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:08Motivational zip example
- 2:55Verification limits
- 4:00Logically qualified types
- 6:57Qualified types syntax
- 7:41Concat example compile checks
- 8:25Predicate language limits
- 10:12Selfification derivation
- 11:37Runtime checks pattern matching
- 13:03Type erasure runtime checks
- 13:49Subtyping rules
- 14:52Solver implementation
- 17:20Future work and SIP
- 17:41Conclusion
- 18:01Q&A
