整數與Peano天然之間的雙向轉換

Question

我在Scala中使用自然數的標準類型編碼。對於這個問題的目的，下面的定義會做到：

sealed trait Nat 
sealed trait _0 extends Nat 
sealed trait Succ[N <: Nat] extends 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 

本工程以這些Nat類型轉換成實際的數字，例如：

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] 

任何想法，爲什麼？

Answer 1

因爲返回類型的int2pair只是Pair而不是Pair { type N = _2 }。 if/else發生在運行時，編譯器無法知道將採取哪個分支。

AFAIK從值到類型的唯一方法是使用宏。你可能想看看shapeless' singleton support。