Granice typu Nat w Shapeless

151

W bezkształtnym typ Nat reprezentuje sposób kodowania liczb naturalnych na poziomie typu. Jest to używane na przykład w przypadku list o stałym rozmiarze. Możesz nawet wykonać obliczenia na poziomie typu, np. Dołączyć listę Nelementów do listy Kelementów i otrzymać listę, która w czasie kompilacji zawiera N+Kelementy.

Czy ta reprezentacja jest w stanie przedstawić duże liczby, np. 10000002 53 , czy też spowoduje to, że kompilator Scala się podda?

Rüdiger Klaehn
źródło
21
Prezentacja Milesa NE Scala w zeszłym roku odnosi się do tego pytania, a krótka odpowiedź jest taka, że ​​byłoby możliwe przedstawienie dużych liczb na poziomie typu w Scali - lub przynajmniej w 2.10 - przy użyciu typów pojedynczych , ale może to nie być tego warte . Shapeless 2.0 nadal używa kodowania Church, co da ci około 1000, zanim kompilator się podda.
Travis Brown
3
Postaram się napisać odpowiedź z nieco szerszym kontekstem później. Na marginesie, praca z typami singletonów całkowitymi nie jest zbyt trudna, jeśli potrzebujesz większych numerów na poziomie typu - zobacz na przykład mój wpis na blogu tutaj lub funkcje singletonów w Shapeless .
Travis Brown
2
Jeśli chcesz wykonywać działania arytmetyczne na dużych liczbach na poziomie typu, możesz rozważyć zaimplementowanie ich jako połączonej listy bitów.
Karol S
1
@KarolS Mam implementację tej strategii! Byłbym szczęśliwy,
mogąc
2
Wygląda na to, że stackoverflow.com/questions/31768203/… został rozwiązany, więc czy możesz dodać swój kod i zamknąć pytanie własną odpowiedzią?
Andriy Kuba

Odpowiedzi:

17

Sam spróbuję. Chętnie przyjmuję lepszą odpowiedź od Travisa Browna lub Milesa Sabina.

Obecnie nie można używać funkcji Nat do reprezentowania dużych liczb

W obecnej implementacji Nat, wartość odpowiada liczbie zagnieżdżonych typów shapeless.Succ []:

scala> Nat(3)
res10: shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]] = Succ()

Tak więc, aby przedstawić liczbę 1000000, miałbyś typ zagnieżdżony na głębokości 1000000 poziomów, co zdecydowanie wysadziłoby kompilator scala. Obecny limit wydaje się wynosić około 400 z eksperymentów, ale dla rozsądnych czasów kompilacji prawdopodobnie najlepiej byłoby pozostać poniżej 50.

Istnieje jednak sposób kodowania dużych liczb całkowitych lub innych wartości na poziomie typu, pod warunkiem, że nie chcesz wykonywać na nich obliczeń . O ile wiem, jedyne, co możesz z nimi zrobić, to sprawdzić, czy są równe, czy nie. Zobacz poniżej.

scala> type OneMillion = Witness.`1000000`.T
defined type alias OneMillion

scala> type AlsoOneMillion = Witness.`1000000`.T
defined type alias AlsoOneMillion

scala> type OneMillionAndOne = Witness.`1000001`.T
defined type alias OneMillionAndOne

scala> implicitly[OneMillion =:= AlsoOneMillion]
res0: =:=[OneMillion,AlsoOneMillion] = <function1>

scala> implicitly[OneMillion =:= OneMillionAndOne]
<console>:16: error: Cannot prove that OneMillion =:= OneMillionAndOne.
       implicitly[OneMillion =:= OneMillionAndOne]
                 ^

Można to wykorzystać np. Do wymuszenia tego samego rozmiaru tablicy podczas wykonywania operacji bitowych na Array [Byte].

Rüdiger Klaehn
źródło
Właśnie zobaczyłem tę odpowiedź i +1, to dobry przykład. Warto jednak zauważyć, że można podać klasy typu, takie jak np. Shapeless, ops.nat.Sumktóre świadczyłyby o tym, że dwie liczby całkowite na poziomie typu miałyby określoną sumę itp. (Wystarczyłoby je podać w makrze).
Travis Brown
1
Oto przykład Concatklasy typu, która umożliwia konkatenację dwóch ciągów na poziomie typu za pomocą makra. Klasa typów do sumowania liczb całkowitych na poziomie typu wyglądałaby prawdopodobnie bardzo podobnie.
Frank S. Thomas
5

Shapeless Natkoduje liczby naturalne na poziomie typu przy użyciu kodowania Church. Alternatywną metodą jest przedstawienie elementów naturalnych jako HList poziomu typu bitów.

Sprawdź gęsty, który realizuje to rozwiązanie w bezkształtnym stylu.

LazyDawno nad tym nie pracowałem i trzeba posypać bezkształtnym „ tu i tam, kiedy Scalac się poddaje, ale koncept jest solidny :)

beefyhalo
źródło