fthomas / fthomas/refined

[discussion] remove shapeless.Nat support

Open
#763 2 comments 0 reactions 0 assignees View on GitHub
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.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.