Бесформенный, как доказать, что Nat находится в границах Size? - PullRequest
Новая
       15

Бесформенный, как доказать, что Nat находится в границах Size?

2 голосов
/ 20 апреля 2019

У нас есть две сущности: одна наша хеш - это число, она представлена ​​Nat, а другая - размерный вектор. Мы хотим, чтобы наш хэш-номер принадлежал одному из элементов размерного вектора. Обычно мы вычисляем желаемый индекс с модом nat % size. 

class SizedVector[A, L <: Nat: ToInt](s: Sized[Vector[A], L]) {
  def shard[Hash <: Nat: ToInt, Index <: Nat](
    hash: Hash32[Hash]
  )(
    implicit
    mod: Mod.Aux[Hash, L, Index],
    index: ToInt[Index]
  ): A = s.at[Index]
}

Как мы можем доказать, что результат мода Index на уровне типа находится в пределах длины размерного вектора? В настоящее время компилятор скажет вам 

could not find implicit value for parameter diff: shapeless.ops.nat.Diff[L,shapeless.Succ[Index]]
): A = s.at[Index]

Предполагается, что он не знает, в чем разница между длиной вектора и вычисленным индексом.

Можно ли обеспечить безопасный доступ и сделать его таким образом?

Scastie: https://scastie.scala -lang.org / kubum / AmbBX3rwQfyXjqRrglYyIg / 5

1 Ответ

3 голосов
/ 20 апреля 2019

Если в компиляторе не хватает неявного, вы добавляете его в качестве параметра.Попробуйте 

def shard[Hash <: Nat: ToInt, Index <: Nat](
  hash: Hash32[Hash]
)(
  implicit
  mod: Mod.Aux[Hash, L, Index],
  index: ToInt[Index],
  diff: Diff[L, Succ[Index]]
): A = s.at[Index]
...