fthomas
Draft macroless ==>
A candidate fix for #755 that refactors ==> to be macroless: if a valid inference cannot be proven, then P1 ==> P2 will fail to manifest. It no longer has a boolean field that is checked via macro.
Introduces a compile-time version of Refined called RefinedLT, which tests a literal type L's value against a corresponding predicate P. So the use of macros has been pushed from ==> to RefinedLT, where the macros are used to extract literal-type value and run the validator against it.
This PR is currently a bit rough - a few unit tests are failing, or failing to compile, which appear to work OK when I run them in the REPL. I also hacked around the old .isValid based unit-testing using a shim that made kittens cry.
I have this passing[*] validateJVM locally, but it has to build against a version of singleton-ops with https://github.com/fthomas/singleton-ops/issues/134, I'm using a publishLocal against head of master.
[*] a few things are disabled
I applause the macroless ==>!
One quick question: Is RefinedLT only required to implement equalValidateInference or are there other reasons or instances it is required for?
@fthomas that's right, I only implemented RefinedLT to solve equalValidateInference. It seemed possibly useful as an implicit tool in its own right. For example, expressing refined-like constraints on type variables. But that's purely speculative.
Probably obvious from the PR diff, and my comments, but worth calling out that this does add singleton-ops as a new dependency.
My thoughts with regards to equalValidateInference: If we accept that the Inference#isValid field was a mistake, then equalValidateInference was a mistake too. The instance was added without explanation in https://github.com/fthomas/refined/commit/f1812d88042b143b826b8ce423d13501a6c1a197 and is in the library since version 0.1.0. I guess my reasoning for adding it was something like this: if Inference requires a Boolean we can go from any value T Refined Equal[U] (which has the value U) to T Refined P by applying P to U to obtain that Boolean. So that instance either requires the questionable isValid field or another macro (RefinedLT). I think if we want to put refined in a better position for Scala 3 we should not trade one macro for another and remove equalValidateInference altogether.
WDYT, @erikerlandson?
I think if we want to put refined in a better position for Scala 3 we should not trade one macro for another and remove equalValidateInference altogether.
@fthomas I have no use cases that would need the equalValidateInference rule. If you are OK with removing it, it seems like a good trade-off for truly reducing the number of macros.
The role of expressing predicate constraints on literal types is arguably the domain of singleton-ops, using forms like OpAuxBoolean[P[T], true]
just as a use-case reference, here is how I'm applying ==> to constrain operations in type sound ways:
https://github.com/erikerlandson/coulomb/blob/refined/coulomb-refined/src/main/scala/coulomb/refined/package.scala#L154
@fthomas I removed RefinedLT and equalValidateInference. There were two impacts.
- this inference is no longer possible:
property("Exists[A] ==> Exists[B]") = secure {
Inference[Contains[W.`'5'`.T], Exists[Digit]].isValid
}
- this assignment no longer compiles
val a: Char Refined Equal[W.`'0'`.T] = '0'
val b: Char Refined Digit = a