Constraint Typing with Boolean Algebra
summary
Claim: Scala 3 union and match types plus inline macros let constraints express full Boolean algebra and be checked compile-time verify or at runtime or left unchecked via guarantee.trust. Prototype implements a Compute typeclass for runtime values and an Inlineable/macro path for compile-time reduction, reuses runtime checks, and demonstrates OR and mutually dependent constraints (e.g. divisor nonzero OR dividend not MinInt). Data types work if constructed as white-box values that retain literal info. Repository exists and the prototype mostly works toward production readiness.
AI-written summary · about
chapters (6)
- 0:00The problem with constraints
- 2:02Limits of refinement types
- 6:15Singleton constraint typing
- 13:03Implementing compile-time checks
- 20:01White-box data representation
- 27:38Conclusion and future outlook
related talks
42mLet the Compiler Help You: How to Make the Most of Scala's Type System
44mType level Computations in Scala
49mThe Trouble With Types
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
14mType-Sensitive Algebraic Macros
28mSecrets of the Scala Type System
33mArmored type safety with Iron
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)