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

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

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

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

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

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


scala type-level-computation peano-numbers
person paradigmatic    schedule 07.01.2013    source источник
comment
Поскольку 2.10 поддерживает только макросы def, я думаю, вам следует взглянуть на макросы типов в раю макросов: docs.scala-lang.org/overviews/macros/paradise.html   -  person Kim Stebel    schedule 07.01.2013
comment
Scala поддерживает зависимые типы? Могу ли я иметь некоторые сведения об этом?   -  person Bill    schedule 13.01.2013
comment
@Bill взгляните на примеры макросов. Тип результата макроса является зависимым типом.   -  person paradigmatic    schedule 13.01.2013
comment
Хм, я никогда не думал об этом таким образом. Это очень круто. Спасибо, @paradigmatic.   -  person Bill    schedule 13.01.2013

Ответы (1)


arrow_upward
8
arrow_downward

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

val holder = NatExample.toNat(13)

А потом:

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

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

person Travis Brown    schedule 07.01.2013
comment
Что означает оператор =:= в этом контексте? - person Dominic Bou-Samra; 07.01.2013
comment
Это класс стандартного библиотечного типа, который предоставляет доказательство того, что компилятор знает, что два типа одинаковы. Это было примерно до 2.10 — см., например, этот ответ для обсуждения того, как он используется. - person Travis Brown; 07.01.2013