Преобразование целых чисел в числа Пеано с использованием системы типов

Question

Это продолжение вопроса, который я задал почти два года назад. Я все еще экспериментирую с системой типов, чтобы написать небольшую библиотеку линейной алгебры, в которой размеры векторов / матриц / тензоров кодируются с использованием системы типов (с нумерацией Пеано). Это позволяет компилятору ограничивать двоичные операции объектами соответствующих измерений.

Это хорошо работает, но я должен указать каждый тип измерения вручную. Например (используя бесформенные натуральные числа):

type _1 = Succ[Nat._0]
type _2 = Succ[_1]
type _3 = Succ[_2]

Это нормально для небольших размеров, но становится скучно, если мне нужно определить размер _1024, Я пытаюсь (без успеха) найти способ преобразовать (во время компиляции) целочисленный литерал в соответствующий тип числа Пеано.

В комментариях Даниэля Собрала мне сказали, что это невозможно, потому что Scala не поддерживает зависимые типы. Теперь Scala 2.10 имеет как зависимые типы, так и макросы. Так есть ли способ достичь этого?

Answer 1

Это возможно прямо сейчас с макросами в 2.10.0 (хотя синтаксис станет чище с Paradise). Я разместил здесь полный рабочий пример - я уверен, что его легко можно сделать гораздо более кратким - который вы можете использовать следующим образом:

val holder = NatExample.toNat(13)

А потом:

scala> implicitly[holder.N =:= shapeless.Nat._13]
res0: =:=[holder.N,shapeless.Nat._13] = <function1>

Это приведет к ошибке с разумной ошибкой во время компиляции, если вы передадите не буквальное целое число и т. Д.