[解決済み] シェイプレスにおけるNat型の限界値

質問

Shapelessでは、Nat型は自然数を型レベルで符号化する方法を表しています。これは例えば固定サイズのリストなどに使われる。型レベルで計算を行うことも可能である。 N のリストに K 要素を持つことがコンパイル時に分かっているリストを返します。 N+K 要素で構成されています。

この表現は、例えば大きな数字を表現することが可能ですか？ 1000000 または2 ⁵³ それとも、これではScalaコンパイラがあきらめてしまうのでしょうか？

どのように解決するのですか？

自分でやってみる。トラヴィス・ブラウンやマイルズ・セービンからより良い答えがあれば、喜んで受け入れるよ。

Nat は現在 <強い ない 大きな数を表現するために使われる

現在の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] に対してビット演算を行う際に、同じ配列サイズを強制するために使用されるかもしれません。