Two-way conversion between integers and Peano naturals

Question

I am using a standard type-encoding of natural numbers in Scala. For the purpose of this question, the following definition will do:

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

I can use the compiler to convert these Nat types into actual numbers, for instance by defining

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

This works:

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

I am trying to invert this correspondence, if possible at all, by exploiting dependent method return types. So, the first thing a need is a container for an Int and a Nat

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

Now, I would like to be able to implicitly convert an Int to an instance of Pair, with the right value for N. Here it is

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
        }
    }

This does compile. Unfortunately

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

fails, as well as

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

Any idea why?

Answer 1

Because the return type of int2pair is just Pair, not Pair { type N = _2 }. The if/else happens at runtime, the compiler can't know which branch will be taken.

AFAIK the only way to go from value to type is with a macro. You might want to look at shapeless' singleton support.