refined integration for scala3 #392
Conversation
|
xref: #385 |
| def plus(x: Refined[V, Positive], y: Refined[V, Positive]): Refined[V, Positive] = | ||
| refineV[Positive].unsafeFrom(alg.plus(x.value, y.value)) |
There was a problem hiding this comment.
what happens if this addition overflows?
There was a problem hiding this comment.
It would be an error, but I haven't worked out a way around it. Technically I think it's type unsound, since if it did overflow it could result in a state not reflected by the type.
There was a problem hiding this comment.
Unless I can check with the validator "manually"
There was a problem hiding this comment.
The only truly type sound semantic would be to have the resulting value be the Either expression, which seems awkward to me, however it would work.
There was a problem hiding this comment.
Well, it "works" in the sense that any type can be a Quantity value, but the algebra typeclass requires the original V type.
There was a problem hiding this comment.
At any rate, the current behavior is NOT unsound
But note that it is unlawful.
There was a problem hiding this comment.
Also probably depends on whether you are semantically trying to represent a modular ring (as in that example) or an unbounded additive semigroup.
There was a problem hiding this comment.
On the bright side, AdditiveSemigroup for + will admit either my algebra definitions or a user's preferred definition, whichever they want to import.
There was a problem hiding this comment.
FWIW, one of my design philosophies has been that the "out-of-box" definitions provided by coulomb deliberately do not try to obscure the "native" behaviors of numeric types. So integer addition can overflow. Floating points do whatever complicated native floating point behaviors, etc.
Users may very reasonably wish to define better semantics, but the definitions of "better" have a lot of potential variation, and I decided it was clarifying to me to avoid that kind of potential for policy explosion.
There was a problem hiding this comment.
Sure. FWIW, the design philosophy of algebra AdditiveSemigroup and friends is that implementing instances are lawful. The laws are the semantics.
|
the "algebraic" policy overlays seem to work: scala> import eu.timepit.refined.*, eu.timepit.refined.api.*, eu.timepit.refined.numeric.*, coulomb.policy.standard.{*, given}, algebra.ring.*, algebra.instances.all.given, coulomb.units.si.{*, given}, coulomb.units.si.prefixes.{*, given}, coulomb.*, coulomb.syntax.*, coulomb.policy.overlay.refined.algebraic.given
scala> refineV[Positive].unsafeFrom(1d).withUnit[Meter]
val res0:
coulomb.Quantity[Double Refined eu.timepit.refined.numeric.Positive,
coulomb.units.si.Meter
] = 1.0
scala> refineV[Positive].unsafeFrom(1).withUnit[Kilo * Meter]
val res1:
coulomb.Quantity[Int Refined eu.timepit.refined.numeric.Positive,
coulomb.units.si.prefixes.Kilo
* coulomb.units.si.Meter] = 1
scala> res0 + res1
val res2:
coulomb.Quantity[Double Refined
eu.timepit.refined.numeric.Greater[shapeless.nat._0]
, coulomb.units.si.Meter] = 1001.0 |
|
Looks very promising. Just yesterday was experimenting with porting some code onto Coulomb, where I divided 24 hours by a short time interval duration, to calculate how many such intervals occur per day. And it made me think that once this refinement is available (for division), the result could be inferred as positive. Currently, I re-assert the result is positive since I don't have inference.. |
erikerlandson
force-pushed
the
refined-scala3
branch
from
aa3e9d9
to
c9c5828
Compare
|
xref fthomas/refined#932 |
|
@erikerlandson If you're willing to cut a beta or RC binary release off this branch sometime, I'd be keen to experiment with it in an application codebase and provide feedback. |
|
I'm a little unsure if you're dependent on changes in Refined to make this viable or if you consider it near usable in present form. |
|
@benhutchison I cut a prerelease 0.7.1-RC1 |
|
@benhutchison regarding fthomas/refined#932, I am not blocked on that. It basically means (for now) I will be providing |
erikerlandson
force-pushed
the
refined-scala3
branch
from
a44be52
to
d46e923
Compare
This initial concept only addresses refined predicates that satisfy algebras such as additive semigroup.