Pursuing Practical Refinement Types by Michael Perucca

"Pursuing Practical Refinement Types" by Michael Perucca at Functional Scala 2022.

This talk presents a refinement-type implementation based on ad hoc subtyping. Scala 3 language features enable great improvements in this area, and Michael analyzes the strengths and weaknesses of such a system. He also explores the advances in compile-time verification of static data, its limitations, and alternatives to achieve a similar level of confidence.

Contents in the video:

00:23 The Problem In a Reduced Form
01:10 Solutions
05:32 Wishlist: What Do I Want?
06:24 The Beginning of an appealing solution
07:17 Trusted or Unchecked Constraint
09:38 Runtime Checking Example
12:50 Compile Time Checking Example
15:23 Constructing Proofs In Steps
17:33 Normalizing Equations with DeMorgan Laws
18:56 A Practical Refinement Type
20:31 Review

#FunScala2022 #scala #zio #functionalprogramming #functionalscala #scalaconference #scaladeveloper

[carnelyve]

Is there a source code somewhere? I would like to learn these techniques

[raphaelfromentin]

How does your approach compares to existing libraries like Refined or Iron?

For example, Iron uses typeclasses with inline methods and seems to satisfy your wishlist:
- Runtime checks for unknowns (via `.refine`, `.refineEither` etc...)
- Compile-time checks (implicit conversion at compile-time between the "normal" type and its refined variant)
- Ability to bypass checking in certain situations via `asInstanceOf`. Maybe a `.assume[Constraint]` would be more elegant than `.asInstanceOf[Type :| Constraint]`?
- User-defined constraint support via typeclasses
- Composable constraints, again, via typeclasses
- Constraint normalization via inline