☰

Shapeless の Nat 型の限界 質問する

tag-icon • tag-icon scala numbers compiler-optimization shapeless
Shapeless の Nat 型の限界 質問する

shapeless では、Nat 型は型レベルで自然数をエンコードする方法を表します。これは、たとえば固定サイズのリストに使用されます。型レベルで計算を行うこともできます。たとえば、N要素のリストに要素のリストを追加しK、コンパイル時に要素があることがわかっているリストを取得しますN+K。

この表現は、たとえば10000002 53などの大きな数値を表すことができますか、それとも Scala コンパイラが諦めてしまうのでしょうか?

ベストアンサー1

私自身も挑戦してみます。Travis Brown または Miles Sabin からのより良い回答を喜んで受け入れます。

ナットは現在ない大きな数を表すために使用される

Nat の現在の実装では、値はネストされた shapeless.Succ[] 型の数に対応します。

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

したがって、1000000 という数値を表現するには、1000000 レベルの深さにネストされた型が必要になりますが、これは間違いなく Scala コンパイラーをクラッシュさせます。実験によると、現在の制限は約 400 のようですが、妥当なコンパイル時間のためには、50 未満に抑えるのがおそらく最善でしょう。

しかし、大きな整数やその他の値を型レベルでエンコードする方法があります。ただし、計算をしたくない場合は私の知る限り、これらを使ってできることは、それらが等しいかどうかを確認することだけです。以下を参照してください。

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]
                 ^

これは、例えばArray[Byte]でビット操作を実行するときに同じ配列サイズを強制するために使用できます。

おすすめ記事