refined support in 0.7 #385
Replies: 8 comments 16 replies
-
|
Agree that the 4 you mention are key and more relevant than other
predicates because they rest on mathematical meaning, and not just
arbitrary boundary points.
There are two others I think are worthy of consideration:
- Fractions [0, 1] Some quite meaningful properties. See also
https://youtu.be/lLUazJS-65k?t=670
- Fractional positive numbers >= 1. A sort of complement to fractions, when
viewed from the perspective of multiplication. Ie multiplying by such a
number grows the output, while multiplying by a fraction shrinks it.
…On Sun, Nov 13, 2022 at 3:15 AM Erik Erlandson ***@***.***> wrote:
cc @armanbilge <https://github.com/armanbilge> @cquiroz
<https://github.com/cquiroz> @benhutchinson
<https://github.com/benhutchinson>
I'm preparing to add support for refined in 0.6, and I wanted to bounce
some thoughts off you.
In 0.5 (scala 2), I supported some fairly rich logic around manipulating
refined predicates. Like adding ">= 1" and ">= 1" could yield an output
with ">= 2", etc.
While I have some interest in continuing to support that kind of clever
type manipulation, I am wondering what the use cases really are.
Because the reality is that I can support the following with much less
effort:
- positive
- non-negative
- negative
- non-positive
Those four I can support with just a few additional algebraic rules for
AdditiveSemigroup (and friends) and ValueResolution , and I have a
suspicion that these cover most use cases.
I wanted to see what you think of that as an initial offering. It doesn't
preclude support for more advanced refined predicate logic in the future,
but I could get this going pretty fast, and the fancy stuff will be
significantly more work.
—
Reply to this email directly, view it on GitHub
<#385>, or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAAXJZCQKT5BFEVDG4LLTA3WH67BRANCNFSM6AAAAAAR6MJUBY>
.
You are receiving this because you are subscribed to this thread.Message
ID: ***@***.***>
|
Beta Was this translation helpful? Give feedback.
-
|
yes, those should also behave as groups or semigroups for multiplication |
Beta Was this translation helpful? Give feedback.
-
|
🤔💭.. a foundation for a future magnitude operation defined over Quantity,
that yields a positive amount associated with some units..
…On Thu, 17 Nov 2022, 12:31 pm Erik Erlandson, ***@***.***> wrote:
#392 <#392>
—
Reply to this email directly, view it on GitHub
<#385 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAAXJZAPYSBZMNF7GJVC7LTWIWDIPANCNFSM6AAAAAAR6MJUBY>
.
You are receiving this because you commented.Message ID:
***@***.***>
|
Beta Was this translation helpful? Give feedback.
-
|
Still thinking about what an implementation of the more general logic might look like. Taking addition as an example, an extension to refined might look like the following transparent inline given ctx_add_refined_2V2U[VL, UL, VR, UR, PL, PR](using
vres: ValueResolution[VL, VR],
icl: Conversion[Quantity[VL, UL], Quantity[vres.VO, UL]],
icr: Conversion[Quantity[VR, UR], Quantity[vres.VO, UL]],
alg: AdditiveSemigroup[vres.VO],
pred: ResolvePredicateAdd[vres.VO, PL, PR]
): Add[Refined[VL, PL], UL, Refined[VR, PR], UR] =
new infra.AddNC((ql: Quantity[Refined[VL, PL], UL], qr: Quantity[Refined[VR, PR], UR]) =>
refinedV[pred.PO].unsafeFrom(alg.plus(icl(ql).value, icr(qr).value)).withUnit[UL]
)where There are also the cases of mixing refined with unrefined values, where the output type should also then be unrefined, or possibly |
Beta Was this translation helpful? Give feedback.
-
|
generalized rules like this would probably be incompatible with the more restrictive algebra based rules above, since there will be cases where either could match and the compiler will fail with ambiguous implicit resolutions. So a user would have to import one or the other. |
Beta Was this translation helpful? Give feedback.
-
|
Almost forgot, conversion factors also impact these. If I have So the |
Beta Was this translation helpful? Give feedback.
-
|
Sorry, took me a little while to circle back to this :) thank you so much for opening the discussion! Since we need refined+coulomb integration, but it wasn't available during the milestone series, we added some of our own helpers here: |
Beta Was this translation helpful? Give feedback.
-
|
I am planning to include these in something like |
Beta Was this translation helpful? Give feedback.
-
|
@armanbilge how is refineMV working with scala 3? this is a known issue upstream: fthomas/refined#932 |
Beta Was this translation helpful? Give feedback.
-
|
We wrote our own implementation. I linked it in that thread. |
Beta Was this translation helpful? Give feedback.
-
|
If I understand what you're doing here, you are proposing an upstream replacement of Given that the state of compile-time |
Beta Was this translation helpful? Give feedback.
-
|
While arbitrary refined predicates like I think the refined types that will prove to have enduring value will be where the refinement reflects an underlying mathematical structure. Probably half the value of the refined type universe is probably embodied in a single predicate, non-negativity. IMO, naturally non-negative quantities almost always arise because we're modeling a magnitude or amount of something. I'd advocate for a slightly more "opinionated" approach, supporting specific refined sets that feature closed operations defined over them. Whereas, for a set like |
Beta Was this translation helpful? Give feedback.
-
|
Agree, as you can see from my thought experiments, supporting "non-algebraic" predicates is a step-function increase in complexity, for what I suspect is very limited benefit. Its primary appeal to me is the "type system cool factor" but I'm going to resist, especially for a first "mvp" release. |
Beta Was this translation helpful? Give feedback.
-
|
another nice property of |
Beta Was this translation helpful? Give feedback.
-
|
one thing I think I could do pretty cleanly is support to wit, the output of scala> refineV[Positive](1)
val res0: Either[String, Int Refined eu.timepit.refined.numeric.Positive] = Right(1)It's possible to define and |
Beta Was this translation helpful? Give feedback.
-
|
I'm going to get the |
Beta Was this translation helpful? Give feedback.
-
|
So in this algebra our quantity objects look like: Quantity[Either[String, Refined[V, P]], U]😂 |
Beta Was this translation helpful? Give feedback.
-
|
The power of algebras - they compose very easily 🎉 |
Beta Was this translation helpful? Give feedback.
-
|
I almost wonder if there is some given given_AS_Either[L, R](using
asL: AdditiveSemigroup[L],
asR: AdditiveSemigroup[R]
): AdditiveSemigroup[Either[L, R]] =
new AdditiveSemigroup[Either[L, R]]:
def plus(x: Either[L, R], y: Either[L, R]): Either[L, R] =
(x, y) match
case (Left(xl), Left(yl)) => Left(asL.plus(xl, yl))
case (Left(xl), Right(_)) => Left(xl)
case (Right(_), Left(yl)) => Left(yl)
case (Right(xr), Right(yr)) => Right(asR.plus(xr, yr)) |
Beta Was this translation helpful? Give feedback.
-
|
For me, the aspect of refinement support that is most exciting is the
fairly rich set of operations that naturally yield or preserve positive
outputs.
Addition, multiplication and division of two positive numbers yields a
positive output. Exponentiation of a positive with any number is positive.
A form of subtraction that yields the distance between two numbers
(unsigned) is always positive.
There will be cases at the boundary of programs to work with Either, but
within the domain model, I hope to establish positivity and then keep it
that way... :)
But I guess this ability to auto-lift Positive => Positive operations into
Either => Either operations makes it close to zero cost to hook up a
refined domain model to an unrefined outside world, where eg strings are
being parsed off the wire..
…On Fri, Nov 25, 2022 at 3:45 AM Erik Erlandson ***@***.***> wrote:
one thing I *think* I could do pretty cleanly is support Either[L,
Refined[V, P]] as an additional overlay.
to wit, the output of refineV is an Either:
scala> refineV[Positive](1)val res0: Either[String, Int Refined eu.timepit.refined.numeric.Positive] = Right(1)
It's possible to define and AdditiveSemigroup on this Either type.
Left + Left => Left
Left + Right(y) => Left
Right(x) + Left => Left
Right(x) + Right(y) => Right(x+y), where x+y is Refined[V, P] + Refined[V, P] - the algebras I am currently defining.
—
Reply to this email directly, view it on GitHub
<#385 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAAXJZD2BUIEMWYOENOCYBDWJ6LTPANCNFSM6AAAAAAR6MJUBY>
.
You are receiving this because you commented.Message ID:
***@***.***>
|
Beta Was this translation helpful? Give feedback.
-
|
good point, you reminded me that positive numbers are a multiplicative group, so I can support division there |
Beta Was this translation helpful? Give feedback.
-
So, distance metric in 1D? |
Beta Was this translation helpful? Give feedback.
-
|
Either a distance metric (my doubt is that I dont recall there being such a thing in Cats Algebra ?), or else an absolute value combined with subtraction might be simpler way of getting to something guaranteed to be positive, ie |a - b| |
Beta Was this translation helpful? Give feedback.
-
cc @armanbilge @cquiroz @benhutchinson
I'm preparing to add support for
refinedin 0.6, and I wanted to bounce some thoughts off you.In 0.5 (scala 2), I supported some fairly rich logic around manipulating refined predicates. Like adding ">= 1" and ">= 1" could yield an output with ">= 2", etc.
While I have some interest in continuing to support that kind of clever type manipulation, I am wondering what the use cases really are.
Because the reality is that I can support the following with much less effort:
Those four I can support with just a few additional algebraic rules for
AdditiveSemigroup(and friends) andValueResolution, and I have a suspicion that these cover most use cases.I wanted to see what you think of that as an initial offering. It doesn't preclude support for more advanced refined predicate logic in the future, but I could get this going pretty fast, and the fancy stuff will be significantly more work.
Beta Was this translation helpful? Give feedback.
All reactions