How using refined to express constraints with constants > 22

Question

I am trying to explore possibilities with refined (and shapeless) to have improved type checking.

I would like to represent, with type, some constraints of interval or size.

So , with refined, i can writes things like that :

type Name = NonEmpty And MaxSize[_32]
type Driver = Greater[_15]

case class Employee(name : String @@ Name, age : Int @@ Driver = refineLit[Driver](18))

But, i would like to express contraints with naturals larger.

type BigNumber = Greater[_1000]

This one doesn't works, because _1000 is not defined. The last one already defined is _22 I can, with shapeless Succ, made my own, but it is very cumbersome.

Example :

type _25 = Succ[Succ[Succ[_22]]]
type _30 = Succ[Succ[Succ[Succ[Succ[_25]]]]]
type _40 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_30]]]]]]]]]]
type _50 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_40]]]]]]]]]]
type _60 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_50]]]]]]]]]]
type _70 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_60]]]]]]]]]]
type _80 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_70]]]]]]]]]]
type _90 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_80]]]]]]]]]]
type _100 = Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[Succ[_90]]]]]]]]]]
// etc.

Is there a better way to express such contraints, or to make _1000 in a more efficient way ? Is there something I would have missed ?

Edit :

I have tried the Travis proposition :

val thousand = shapeless.nat(1000)

But this line causes a StackOverflowError at compile time (at macro expansion) If I try with a lesser number, it is ok.

val limit = shapeless.nat(50)
type BigNumber = Greater[limit.N]

case class TestBigNumber(limit : Int @@ BigNumber)

In my environment, the StackOverflowError is raised for numbers greater than 400.

Moreover, with this code, compilation never ended (using sbt) :

val n_25 = shapeless.nat(25)
type _25 = n_25.N

val n_32 = shapeless.nat(32)
type _32 = n_32.N

val n_64 = shapeless.nat(64)
type _64 = n_64.N

Answer 1

The Greater predicate in refined supports both Shapeless's type-level natural numbers (Nat) and integer singleton types (which are made available by Shapeless's Witness). So the following constraints do the same thing:

import eu.timepit.refined.implicits._
import eu.timepit.refined.numeric._
import shapeless.{ Nat, Witness }
import shapeless.tag.@@

val a: Int @@ Greater[Nat._10] = 11
val b: Int @@ Greater[Witness.`10`.T] = 11

Because of the ways Nat and integer singleton types are represented, the latter are much less likely to make the compiler overflow the stack. For example, the following works on my machine:

scala> val c: Int @@ Greater[Witness.`10000`.T] = 10001
c: shapeless.tag.@@[Int,eu.timepit.refined.numeric.Greater[Int(10000)]] = 10001

Even though 10000 is well past the point where shapeless.nat(10000) starts to stack overflow.

---

As a footnote, it is possible to use the Nat representation for values larger than 22 without just typing Succ a lot:

val hundred = shapeless.nat(100)
val c: Int @@ Greater[hundred.N] = 101

This is still going to blow the stack for large values, though, so the integer singleton types are the way to go in your case.