Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[discussion] remove shapeless.Nat support #763

Open
erikerlandson opened this issue Apr 16, 2020 · 2 comments · Fixed by #848
Open

[discussion] remove shapeless.Nat support #763

erikerlandson opened this issue Apr 16, 2020 · 2 comments · Fixed by #848

Comments

@erikerlandson
Copy link
Contributor

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
Copy link
Contributor Author

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.

@fthomas
Copy link
Owner

fthomas commented Sep 25, 2020

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 #483. #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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants