Limites de type Nat dans Shapeless

Dans l’informe, le type Nat représente un moyen d’encoder des nombres naturels au niveau d’un type. Ceci est utilisé par exemple pour les listes de taille fixe. Vous pouvez même faire des calculs au niveau du type, par exemple, append une liste de N éléments à une liste de K éléments et récupérer une liste connue au moment de la compilation pour avoir N+K éléments.

Cette représentation est-elle capable de représenter des nombres importants, par exemple 1000000 ou 2 ⁵³ , ou le compilateur Scala va-t-il abandonner?

Je vais essayer un moi-même. J’accepterai volontiers une meilleure réponse de Travis Brown ou Miles Sabin.

Nat ne peut actuellement pas être utilisé pour représenter des nombres importants

Dans l’implémentation actuelle de Nat, la valeur correspond au nombre de types nesteds sans forme.

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

Donc, pour représenter le nombre 1000000, vous auriez un type nested 1000000 niveaux profonds, ce qui ferait exploser le compilateur Scala. La limite actuelle semble être d’environ 400 pour l’expérimentation, mais pour des temps de compilation raisonnables, il serait probablement préférable de restr en dessous de 50.

Cependant, il existe un moyen d’encoder des entiers volumineux ou d’autres valeurs au niveau du type, à condition que vous ne souhaitiez pas effectuer de calculs sur ces entiers. Pour autant que je sache, la seule chose à faire est de vérifier si elles sont égales ou non. Voir ci-dessous.

 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] =  scala> implicitly[OneMillion =:= OneMillionAndOne] :16: error: Cannot prove that OneMillion =:= OneMillionAndOne. implicitly[OneMillion =:= OneMillionAndOne] ^

Cela pourrait être utilisé pour, par exemple, appliquer la même taille de tableau lors d’opérations de bits sur Array [Byte].

Nat code les nombres naturels au niveau du type en utilisant l’encodage de l’église. Une autre méthode consiste à représenter les naturals au niveau du type HList des bits.

Découvrez dense qui implémente cette solution dans un style informel.

Je n’y ai pas travaillé depuis un moment, et il a besoin de saupoudrer de Lazy ici et là pour que le scalac abandonne, mais le concept est solide 🙂