Как использовать уточнение для выражения ограничений с помощью констант › 22

Я пытаюсь изучить возможности с уточнением (и бесформенностью), чтобы улучшить проверку типов.

Я хотел бы представить типом некоторые ограничения интервала или размера.

Итак, с уточнением я могу писать такие вещи:

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

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

Но я хотел бы выразить ограничения с помощью натуральных чисел большего размера.

type BigNumber = Greater[_1000]

Это не работает, потому что _1000 не определено. Последний уже определенный _22 Я могу с бесформенным Succ сделать свой, но очень громоздкий.

Пример :

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.

Есть ли лучший способ выразить такие ограничения или сделать _1000 более эффективным способом? Есть ли что-то, что я бы пропустил?

Изменить :

Я попробовал предложение Трэвиса:

val thousand = shapeless.nat(1000)

Но эта строка вызывает StackOverflowError во время компиляции (при расширении макроса). Если я попробую с меньшим числом, все в порядке.

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

case class TestBigNumber(limit : Int @@ BigNumber)

В моей среде StackOverflowError возникает для чисел больше 400.

Более того, с этим кодом компиляция никогда не заканчивалась (с использованием 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

scala shapeless
person volia17    schedule 01.07.2015    source источник
comment
Вы можете использовать val thousand = nat(1000); type BigNumber = Greater[thousand.N], что немного лучше. Я думал, что можно написать что-то вроде Nat.`100`.N, но, возможно, мне это показалось.   -  person Travis Brown    schedule 01.07.2015
comment
@travis: у меня возникает StackOverflowError во время раскрытия макроса в строке val thousand = nat(1000), как в eclipse, так и в sbt   -  person volia17    schedule 01.07.2015

Ответы (1)


arrow_upward
10
arrow_downward

Предикат Greater в refined поддерживает как натуральные числа Shapeless на уровне типов (Nat), так и целочисленные одноэлементные типы (которые доступны благодаря Shapeless Witness). ). Таким образом, следующие ограничения делают то же самое:

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

Из-за способов представления Nat и целочисленных одноэлементных типов последние с гораздо меньшей вероятностью вызовут переполнение стека компилятором. Например, на моей машине работает следующее:

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

Несмотря на то, что 10000 уже далеко за точкой, где shapeless.nat(10000) начинает переполняться стек.

В качестве сноски можно использовать представление Nat для значений больше 22, не набирая много Succ:

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

Тем не менее, это по-прежнему будет взорвать стек для больших значений, поэтому в вашем случае подойдут целочисленные одноэлементные типы.

person Travis Brown    schedule 01.07.2015
comment
Спасибо, стало намного лучше. Но, поскольку всегда есть но, этот код хорошо компилируется с sbt, но у меня есть ошибка в eclipse stable identifier required, but shapeless.Witness.selectDynamic("32") found. - person volia17; 01.07.2015
comment
@ volia17 Извините, мои знания Eclipse практически отсутствуют, и я не возражаю против того, чтобы так и оставалось. :) Наверное стоит новый вопрос? - person Travis Brown; 01.07.2015
comment
В качестве обходного пути вы можете попробовать val tenThousand = Witness.`10000`, а затем Greater[tenThousand.T]. - person Travis Brown; 01.07.2015
comment
+1 Отличный ответ. :-) Думаю, мне нужно лучше задокументировать, что все числовые предикаты работают с Nat и числовыми одноэлементными типами. Удивительная вещь в одноэлементных типах заключается в том, что в этих предикатах также можно использовать Double, например. Double @@ Greater[Witness.`0.5`.T] - person Frank S. Thomas; 01.07.2015