[discussion] remove shapeless.Nat support
- Dominant language
- Scala
- Stars
- 1.7k
- Forks
- 152
- Avg merge
- 1h 20m
- Merged PRs (30d)
- 6
Description
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:
```scala
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`.
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.