Explore constraint typing with Boolean algebra in this Scala Days 2023 Seattle conference talk. Delve into how Scala 3's new features enable a composable constraint system that supports the full breadth of Boolean algebra. Learn about the limitations of primitive types in conveying sufficient constraints for safe function calls, and discover how to specify additional constraints on data types without changing them. Examine the drawbacks of under-constrained data specification and traditional refinement type approaches. Understand how union and match types in Scala 3 allow for user-defined constraints that can be evaluated at runtime or compile-time through inlining. Follow along as the speaker demonstrates the implementation of a singleton constraint typing system, showcasing the shift from black box to white box paradigms. Gain insights into embracing literal types and handling data types with internal structures. Suitable for software engineers interested in advanced typing techniques and program correctness in Scala.
Overview
Syllabus
Intro
Programming without constraints
Compile time enforced constraints?
Refinement example: underconstrained
"Traditional" Refinement System Insight
Singleton Constraint Typing: Test
First Implement the Computation
Implement Compile Time Verification
Black Box to White Box Paradigm Shift
Embracing Literal Types
Data Type with Internal Structure (w/ error)
Summarizing the Key Ideas
Taught by
Scala Days Conferences
