shapeless では、Nat 型は型レベルで自然数をエンコードする方法を表します。これは、固定サイズのリストなどに使用されます。型レベルで計算を行うこともできます。たとえば、要素のリストをN
要素のリストに追加しK
、コンパイル時にN+K
要素を持つことがわかっているリストを取得します。
1000000
この表現は2 53などの大きな数を表すことができますか、それとも Scala コンパイラーがあきらめる原因になりますか?
shapeless では、Nat 型は型レベルで自然数をエンコードする方法を表します。これは、固定サイズのリストなどに使用されます。型レベルで計算を行うこともできます。たとえば、要素のリストをN
要素のリストに追加しK
、コンパイル時にN+K
要素を持つことがわかっているリストを取得します。
1000000
この表現は2 53などの大きな数を表すことができますか、それとも Scala コンパイラーがあきらめる原因になりますか?
私は自分で試してみます。Travis Brown または Miles Sabin からのより良い回答を喜んで受け入れます。
現在、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] でビット操作を行うときに同じ配列サイズを強制するために使用できます。
ShapelessNat
は、Church エンコーディングを使用して型レベルで自然数をエンコードします。もう 1 つの方法は、ナチュラルをビットのタイプ レベル HList として表すことです。
このソリューションを形のないスタイルで実装するdenseをチェックしてください。
私はしばらくそれに取り組んでいませんでしLazy
た.scalacがあきらめたときのために、あちこちにshapelessを振りかける必要がありますが、コンセプトはしっかりしています:)