Двунаправленное преобразование между целыми числами и перьями Пеано

Question

Я использую стандартное кодирование натуральных чисел в Scala. Для целей данного вопроса, следующее определение будет делать:

sealed trait Nat 
sealed trait _0 extends Nat 
sealed trait Succ[N <: Nat] extends Nat 

Я могу использовать компилятор для преобразования этих Nat типов в реальные цифры, например, путем определения

class NatConverter[N <: Nat](val n: Int) 

implicit val zeroConv: NatConv[_0] = new NatConv(0) 
implicit def succConv[N <: Nat](implicit ev: NatConv[N]): NatConv[Succ[N]] = 
    new NatConv(ev.n + 1) 

def nat2value[N <: Nat](implicit ev: NatConv[N]) = ev.n 

Это работает:

type _1 = Succ[_0] 
type _2 = Succ[_1] 
nat2value[_2] // gives 2 

Я пытаюсь инвертировать это соответствие, если возможно вообще, используя типы возвращаемых зависимых методов. Итак, первое, что необходимо является контейнером для Int и Nat

trait Pair { 
    type N <: Nat 
    def n: Int 
} 

Теперь, я хотел бы быть в состоянии неявно преобразовать Int к экземпляру Pair, с правильным значением для N. Здесь

implicit def int2pair(a: Int): Pair = 
    if (a == 0) new Pair { 
     type N = _0 
     val n = 0 
    } 
    else { 
     val previous = int2pair(a - 1) 
     new Pair { 
      type N = Succ[previous.N] 
      val n = a 
     } 
    } 

Это компилируется. К сожалению

val two = int2pair(2) 
implicitly[two.N =:= _2] 

выходит из строя, а также

val two = int2pair(2) 
implicitly[two.N <:< _2] 

Любая идея, почему?

Answer 1

Поскольку тип возвращение из int2pair просто Pair, не Pair { type N = _2 }. if/else происходит во время выполнения, компилятор не может знать, какая ветка будет занята.

AFAIK единственный способ перейти от значения к типу с макросом. Вы можете посмотреть на shapeless' singleton support.