refined icon indicating copy to clipboard operation
refined copied to clipboard

[discussion] remove shapeless.Nat support

Open erikerlandson opened this issue 4 years ago • 2 comments

I don't know all the context or use cases for shapeless.Nat support in refined (or singleton-ops), but superficially the ability to write TypeName[3] makes something like TypeName[shapeless.nat._3] obsolete.

It has some implications for how refined currently works. For example the following compiles: refineV[Greater[_4]](5D) but this does not: refineV[Greater[4]](5D)

It would probably require allowing Int literal-types to replace Nat as the "universal" numeric predicate argument. Or possibly not having a universal argument, which would make Positive or NonNegative infeasible as they currently work. Possibly replaced with Positive[Int], etc.

At the type/implicit level, it is also conceivable to map all literal-type values ToDouble under the hood. An example code fragment from a different experiment:

    implicit def impliesGTGT[L, R, LD <: XDouble, RD <: XDouble](implicit
        ld: OpAuxDouble[ToDouble[L], LD],
        rd: OpAuxDouble[ToDouble[R], RD],
        q: OpAuxBoolean[LD >= RD, true]): Greater[L] ==> Greater[R] =
      new Implies[Greater[L], Greater[R]] {}

This casting should actually be lossless for every value except Long >= 2^53. I am unsure if doing this is desirable compared to requiring numeric type values to all match up, but it is feasible and might eliminate some rule systems duplicated across Int,Long,Float,Double.

erikerlandson avatar Apr 16 '20 22:04 erikerlandson

note the above implementation of impliesGTGT only makes sense if something like Greater[N] operates by converting both N and the argument to be tested into double, and doing the test in double space. There are legit arguments against that policy, but it is workable to do it.

erikerlandson avatar Apr 16 '20 23:04 erikerlandson

Using Nat as universal numeric predicate argument is indeed the only reason why it is still supported. It is nice that one definition of Positive can be used for all numeric types from Byte to BigDecimal.

It would probably require allowing Int literal-types to replace Nat as the "universal" numeric predicate argument.

This got me thinking how hard it would be to do this. It turned out not so much since the introduction of WitnessAs in https://github.com/fthomas/refined/pull/483. https://github.com/fthomas/refined/pull/841 adds the required WitnessAs instances so that Int literals can now be used as arguments for any numeric base type and Double literals for fractional base types, for example:

scala> refineV[Greater[4]](5.toByte)
val res1: Either[String,eu.timepit.refined.api.Refined[Byte,eu.timepit.refined.predicates.all.Greater[4]]] = Right(5)

scala> refineV[Greater[4]](5D)
val res2: Either[String,eu.timepit.refined.api.Refined[Double,eu.timepit.refined.predicates.all.Greater[4]]] = Right(5.0)

scala> refineV[Greater[2.718]](BigDecimal(3.145))
val res3: Either[String,eu.timepit.refined.api.Refined[scala.math.BigDecimal,eu.timepit.refined.predicates.all.Greater[2.718]]] = Right(3.145)

The first and third example are especially interesting since there are no Byte or BigDecimal literals in the language so these refinements could not be expressed before.

fthomas avatar Sep 25 '20 20:09 fthomas