Sum of HList (where all elements are Nat's) I wrote the following to output, at the type level, the sum, Nat, of an input HList:

trait HListSum[L] {
  type Out
}
object HListSum {

  type Aux[L, O] = HListSum[L] { type Out = O }

  def apply[L &lt;: HList](implicit ev: HListSum[L]): ev.type = ev

  implicit def hListSumInductive[H &lt;: Nat, L &lt;: HList, S &lt;: Nat, T &lt;: Nat](
    implicit rest: HListSum.Aux[L, T],
             all: Sum.Aux[H, T, S]): HListSum.Aux[H :: L, S] = new HListSum[H :: L] {
    type Out = S
  }

  implicit val hlistSumHNil: HListSum.Aux[HNil, _0] = new HListSum[HNil] {
    type Out = _0
  }
}


Testing:

import net.HListSum
import shapeless._
import nat._

scala&gt; HListSum[_1 :: _2 :: _3 :: HNil]
res0: net.HListSum.Aux[shapeless.::[shapeless.nat._1,shapeless.::[shapeless.nat._2,shapeless.::[shapeless.nat._3,shapeless.HNil]]],this.Out] = net.HListSum$$anon$4@132c4879

scala&gt; val expected: res0.Out = _6
expected: res0.Out = Succ()

scala&gt; HListSum[_0 :: _0 :: _1 :: HNil]
res1: net.HListSum.Aux[shapeless.::[shapeless.nat._0,shapeless.::[shapeless.nat._0,shapeless.::[shapeless.nat._1,shapeless.HNil]]],this.Out] = net.HListSum$$anon$4@a7b83a8

scala&gt; val expected2: res1.Out = _1
expected2: res1.Out = Succ()

scala&gt; val expected2: res1.Out = _3
&lt;console&gt;:19: error: type mismatch;
 found   : shapeless.nat._3
    (which expands to)  shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]
 required: res1.Out
    (which expands to)  shapeless.Succ[shapeless._0]
       val expected2: res1.Out = _3
                                 ^


Please critique my code. Also, am I using induction to determine the sum for the non-HNil case?
First for some little things. I'd put bounds on the L type parameter and the Out type member to capture the facts that you know will always be true about them:

trait HListSum[L &lt;: HList] {
  type Out &lt;: Nat
}


This makes the intent clearer to readers and allows you to use Out in places you couldn't otherwise—e.g. this simple example wouldn't compile without the bound:

scala&gt; def foo[N &lt;: Nat]: Unit = ()
foo: [N &lt;: shapeless.Nat]=&gt; Unit

scala&gt; def bar[L &lt;: HList](implicit sum: HListSum[L]): Unit = foo[sum.Out]
bar: [L &lt;: shapeless.HList](implicit sum: HListSum[L])Unit


I'd also change the return type of apply to be a little more specific (or rather less specific, I guess—more focused on what's relevant, in any case):

def apply[L &lt;: HList](implicit ev: HListSum[L]): Aux[L, ev.Out] = ev


This is mostly for legibility—apart from how the type is printed in the console I'm not sure off the top of my head whether there's any real difference between this and the ev.type version.

I'd make two changes to the hListSumInductive implementation (apart from changing the case of the l in the name to be consistent with hlistSumHNil):

implicit def hlistSumInductive[H &lt;: Nat, T &lt;: HList, TS &lt;: Nat](implicit
  rest: HListSum.Aux[T, TS],
  all: Sum[H, TS]
): HListSum.Aux[H :: T, all.Out] = new HListSum[H :: T] {
  type Out = all.Out
}


The first is that I've renamed L to T and T to TS, since using H and T to name the head and tail types of an hlist is a pretty standard convention. More significantly, I've dropped the S type parameter (representing the total sum) altogether, since we don't need a type parameter to refer to that type (all.Out works just fine, since we don't need to refer to it in other implicit parameters).

One other note about this method: I'm not sure whether you chose Sum[H, TS] over Sum[TS, H] intentionally, but it's the right thing to do if you care about compile times (and you should in a case like this), since the instance will be resolved more quickly when the larger number is on the right, and in this operation the larger number will be TS more often.

One other tiny thing—I'd probably rename O in Aux:

type Aux[L &lt;: HList, Out0] = HListSum[L] { type Out = Out0 }


Mostly because O is easy to confuse with 0, and because I personally tend to use the 0 suffix as a convention in these cases. That's entirely a matter of taste, though.

Lastly, if I were writing this for a library I'd probably use a sealed abstract class instead of a trait and would make the object final, but neither change is terribly important.