纳特types的限制在无形中
在无形中，Nattypes表示一种在types级别编码自然数的方法。 这用于例如固定大小的列表。 你甚至可以在types层次上进行计算，例如在K元素列表中追加N元素的列表，并获得在编译时已知的具有N+K元素的列表。
这种表示能够表示大数字，例如1000000或2 53 ，还是这会导致Scala编译器放弃？
我会自己尝试一个。 我会很乐意接受Travis Brown或Miles Sabin的更好的回答。
纳特目前不能用来表示大数字
在Nat的当前实现中，该值对应于嵌套的shapeless.Succ []types的数目：
scala> Nat(3) res10: shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]] = Succ()
所以要表示数字1000000，你将有一个嵌套1000000级别的types，这肯定会炸毁scala编译器。 目前的限制似乎是从实验400左右，但在合理的编译时间，可能最好保持在50以下。
但是， 如果您不想对它们进行计算，则可以在types级别对大整数或其他值进行编码。 我所知道的唯一可以做的就是检查它们是否平等。 见下文。
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]上执行位操作时强制执行相同的数组大小。
无形的Nat使用教会编码在types级别编码自然数。 另一种方法是将自然表示为位级的HList。
检查密度 ，实现这个解决scheme在一个不成形的风格。
我有一段时间没有工作，它需要一个不成形的“当懒惰放弃时，在这里和那里，但这个概念是坚实的 🙂
