Límites de tipo Nat en Shapeless

151

En sin forma, el tipo Nat representa una forma de codificar números naturales a nivel de tipo. Esto se usa, por ejemplo, para listas de tamaño fijo. Incluso puede hacer cálculos a nivel de tipo, por ejemplo, agregar una lista de Nelementos a una lista de Kelementos y recuperar una lista que se sabe que en el momento de la compilación tiene N+Kelementos.

¿Es esta representación capaz de representar grandes números, por ejemplo, 1000000o 2 ⁵³ , o esto hará que el compilador Scala se rinda?

scala numbers compiler-optimization shapeless Rüdiger Klaehn
fuente

La presentación de Miles Scala NE el año pasado aborda esta pregunta, y la respuesta corta es que sería posible representar grandes números a nivel de tipo en Scala, o al menos en 2.10, usando tipos singleton , pero puede que no valga la pena . Shapeless 2.0 actualmente todavía usa la codificación Church, que lo llevará a aproximadamente 1,000 antes de que el compilador se dé por vencido.

Travis Brown el

Trataré de escribir una respuesta con un poco más de contexto más tarde hoy. Como nota al margen, no es demasiado difícil trabajar con tipos de singleton enteros si necesita números de nivel de tipo más grandes; consulte, por ejemplo, mi publicación de blog aquí o la funcionalidad de singleton en Shapeless .

Travis Brown el

Si desea hacer aritmética en números grandes de nivel de tipo, puede considerar implementarlos como una lista vinculada de bits.

Karol S

@KarolS ¡Tengo una implementación de esa estrategia! Y me alegraría contribuir a sin forma si alguien está interesado, aunque no vale nada a menos que alguien pueda ayudar a resolver stackoverflow.com/questions/31768203/…

beefyhalo

Parece que stackoverflow.com/questions/31768203/… está resuelto, así que ¿puedes aportar tu código y cerrar la pregunta con tu propia respuesta?

Andriy Kuba

Respuestas:

Intentaré uno yo mismo. Con mucho gusto aceptaré una mejor respuesta de Travis Brown o Miles Sabin.

Nat no se puede usar actualmente para representar grandes números

En la implementación actual de Nat, el valor corresponde al número de tipos anidados sin forma.Succ []:

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

Por lo tanto, para representar el número 1000000, tendría un tipo anidado con niveles de 1000000 de profundidad, lo que definitivamente haría explotar el compilador de scala. El límite actual parece ser de aproximadamente 400 por experimentación, pero para tiempos de compilación razonables probablemente sería mejor mantenerse por debajo de 50.

Sin embargo, hay una manera de codificar enteros grandes u otros valores a nivel de tipo, siempre que no desee hacer cálculos sobre ellos . Hasta donde yo sé, lo único que puede hacer es comprobar si son iguales o no. Vea abajo.

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

Esto podría usarse, por ejemplo, para imponer el mismo tamaño de matriz cuando se realizan operaciones de bits en Array [Byte].

Rüdiger Klaehn
fuente

Acabo de ver esta respuesta, y +1, este es un buen ejemplo. Sin embargo, vale la pena señalar que podría proporcionar clases de tipos como, por ejemplo, Shapeless ops.nat.Sumque presenciarían que dos enteros de nivel de tipo tenían una suma particular, etc. (solo tendrían que ser proporcionados por una macro).

Travis Brown

Aquí hay un ejemplo de una Concatclase de tipo que permite concatenar dos cadenas de nivel de tipo a través de una macro. Una clase de tipo para sumar enteros de nivel de tipo probablemente se vería muy similar.

Frank S. Thomas

Shapeless's Natcodifica números naturales en el nivel de tipo usando la codificación Church. Un método alternativo es representar los naturales como una lista de bits de nivel de tipo.

Echa un vistazo a denso que implementa esta solución en un estilo sin forma.

No he trabajado en eso en mucho tiempo, y necesita una pizca de ' Lazyaquí y allá sin forma para cuando Scalac se rinda, pero el concepto es sólido :)

beefyhalo
fuente