Integrate with Refined about coulomb HOT 5 CLOSED

There are two basic approaches here, which could be described as:

1. Refined is inside Quantity
2. Refined is outside Quantity

I'm coming to the conclusion that the first is the more useful. However, the current Quantity design has baked in an implicit of Numeric[N] for a lot of operations, which works against putting Refined inside as-is.

If I factor out operations into an implicit class, I believe it will pave the way for supporting Quantity[Refined[N, P], U] in a more extensible way.

Such a refactorization is likely to represent a 0.5.x release series

from coulomb.

Closure. Refined values do not appear to be closed under arithmetic operations, which is sensible since in general doing operations on a value isn't guaranteed to preserve whatever refined predicates are in effect.

scala> val xx: Int Refined NonNegative = 2
xx: eu.timepit.refined.api.Refined[Int,eu.timepit.refined.numeric.NonNegative] = 2

scala> xx + 1
res23: Int = 3

Probably the same should be true for quantities of the form Quantity[Refined[N, P], U] - if some operation is applied then the result has type Quantity[N, U]

@fthomas I'm curious if you have any insights or opinions.

from coulomb.

You're correct about operations on refined types in general. Applying operations on refined values might make them invalid according to the predicate. But for some numeric refined types additive Semigroup / Monoid instances are provided which overflow according to their predicate:

scala> PosInt.MaxValue |+| PosInt(1)
res5: eu.timepit.refined.types.numeric.PosInt = 1

scala> NonNegInt.MaxValue |+| NonNegInt(1)
res6: eu.timepit.refined.types.numeric.NonNegInt = 0

Regarding if Refined should be inside Quantity or the other way round, I just want to note that most libraries that provide integration with refined are providing instances of their type classes for refined types so in these case Refined is always inside their type classes. But I don't have enough experience with coulomb to have an informed opinion on this matter. I guess you could argue for both depending on your predicate if it is refining the quantity/unit or just the value of the quantity.

from coulomb.

I have a solution for addressing closure. For Postive and NonNegative there are proper closed algebras for additive and multiplicative Semigroups/Monoids. These can be supported in a type-sound manner by default: if type checking compiles, there should be no runtime failures(*)

I will also support un-sound operations, on an opt-in basis. These are also properly validated for refined predicates, but at run-time, not compile time.

(*) there will actually be a couple edge cases here: division by zero in the case of NonNegative, and for Positive it will be possible for some unit conversions to round-down to zero, particularly when working with integer types.

from coulomb.

Implemented on release 0.4.5 (#73)

from coulomb.