Sabitler> 22

Question

ile kısıtlamaların ifade edilmesi nasıl geliştirilir Gelişmiş tip kontrolüne sahip olmak için rafine edilmiş (ve şekilsiz) olasılıkları araştırmaya çalışıyorum.

Aralıkla, bazı aralık veya boyut kısıtlamalarını temsil etmek istiyorum. i naturals büyüğüyle contraints ifade etmek isterim,

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

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

Ama:

Yani, rafine ile, i can böyle şeyler yazıyor. _1000 tanımlanmamış nedeniyle

type BigNumber = Greater[_1000] 

Bu seferki, program çalışmaz. Sonuncusu zaten tanımlanmış olan _22 Ben Succ şekilsiz, kendim yaptı, ama çok hantal.

Örnek:

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. 

böyle contraints ifade etmek ya da daha verimli bir şekilde _1000 yapmak için daha iyi bir yolu var mı? Kaçırdığım bir şey var mı?

Düzenleme: Travis önermeyi denedi

: Ben daha az sayı ile çalışırsanız

val thousand = shapeless.nat(1000) 

Fakat bu çizgi (makro genişleme de) derleme zamanında bir StackOverflowError neden , onu tamam. Benim ortamda

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

case class TestBigNumber(limit : Int @@ BigNumber) 

, StackOverflowError bu kod, derleme sona asla (kullanarak sbt) ile, 400 Dahası

daha büyük sayılar için yükseltilir:

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

Greater yüklem içinde refined, Shapeless'in tür düzeyindeki doğal sayıları (Nat) ve tamsayı singleton türlerini destekler (bunlar Shapeless'in Witness tarafından kullanılabilir). Yani aşağıdaki kısıtlamalar aynı şeyi yapmak: Çünkü yollar Nat ve tamsayı tekil türlerinden

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 

temsil edilir, ikincisi çok daha az olası derleyici taşması yığın yapmak için vardır. Örneğin, benim makinede aşağıdaki çalışır:

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

bile 10000 olsa iyi shapeless.nat(10000) başlar taşması yığın noktaya geçmiş.Bir dipnot olarak

---

, sadece Succ çok yazmadan 22 daha büyük değerler için Nat temsilini kullanmak mümkündür: Bu hala büyük değerler için yığın patlayacak

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

, Yine de, tamsayı singleton türleri sizin davanıza girmenin yolu.