Int value of Prod in shapeless

Question

Playing around with shapeless natural numbers in excitement, I wonder what could be the best approach to getting the integer value of e.g. a product of nats.

Excerpt from shapeless nat.scala:

trait Prod[A <: Nat, B <: Nat] {
  type Out <: Nat
}

trait ProdAux[A <: Nat, B <: Nat, C <: Nat]

object Prod {
  implicit def prod[A <: Nat, B <: Nat, C <: Nat](implicit diff : ProdAux[A, B, C]) = new Prod[A, B] {
    type Out = C
  }
}

object ProdAux {
  import Nat._0

  implicit def prod1[B <: Nat] = new ProdAux[_0, B, _0] {}
  implicit def prod2[A <: Nat, B <: Nat, C <: Nat, D <: Nat]
    (implicit ev1 : ProdAux[A, B, C], ev2 : SumAux[B, C, D]) = new ProdAux[Succ[A], B, D] {}
}

So far I've come up with the straightforward definition of

def toInt[A <: Nat, B <: Nat, C <: Nat](p: Prod[A, B])
    (implicit paux: ProdAux[A, B, C], iv: ToInt[C]): Int = iv()

As a matter of fact that approach would require somewhat redundant implementations of the equivalent code for e.g. sums, diffs, factorials etc. So I'd rather be able to use the "default" method toInt[A <: Nat].

How would you do it? And is it possible to use the inner types (Prod#Out, Sum#Out, ...)?

Answer 1

Sorry I missed this question earlier (BTW, the shapeless mailing list is a good place to ask this kind of question).

I think you've slightly misunderstood the role of the Prod type class: its instances aren't themselves Nats, they're witnesses of a relation holding between three Nats, namely that (A * B) == C. As such, it doesn't really make all that much sense to convert Prod instances to Ints. Or rather, if it did, it'd make just as much sense for the resulting value to correspond to any of A, B or C, or the triple of all of them.

For use as proof terms in method definitions, the style you've shown is pretty much as intended ... see here for an example. Clearly though, this doesn't work very well for playing around with things on the REPL. To make that a bit smoother you could try things along the lines of,

def prod[A <: Nat, B <: Nat](implicit prod : Prod[A, B]) =
  new { def toInt(implicit ti : ToInt[prod.Out]) = ti() }

which allows REPL interactions like,

scala> prod[_2, _3].toInt
res0: Int = 6

If this still isn't quite what you're after then please head over to the mailing list and sketch out what you'd like to be able to do.