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
The biggest difference is that Refined and Iron both attach refinements by modifying the refined value's type (whether by opaque types, tagging, etc.). This becomes cumbersome when specifying mutually dependent refinements, requiring grouping values together to attach the refinement, as a refinement can only refine a single value. The alternative here is to move the refinement (probably better referred to as a constraint) to a separate predicate. The predicates refer to the refined values through singleton types, allowing the values to keep their original type, also permitting mutually dependent constraints naturally. A separate constraint predicate is just like a Boolean equation with the singleton types as the variables, and it composes more easily than attaching constraints by modifying the constrained values' types. Another difference is that Refined and Iron both support some form of implication. I chose not to try to support that with this approach.
Is there a source code somewhere? I would like to learn these techniques
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
The biggest difference is that Refined and Iron both attach refinements by modifying the refined value's type (whether by opaque types, tagging, etc.). This becomes cumbersome when specifying mutually dependent refinements, requiring grouping values together to attach the refinement, as a refinement can only refine a single value. The alternative here is to move the refinement (probably better referred to as a constraint) to a separate predicate. The predicates refer to the refined values through singleton types, allowing the values to keep their original type, also permitting mutually dependent constraints naturally. A separate constraint predicate is just like a Boolean equation with the singleton types as the variables, and it composes more easily than attaching constraints by modifying the constrained values' types.
Another difference is that Refined and Iron both support some form of implication. I chose not to try to support that with this approach.