KataBankOCR checksum at the type level

kata-bank-ocr.scala

/**
 * We can use the Scala type system (with help from Miles Sabin's Shapeless
 * library) to solve the bank account number validation problem in the second
 * user story of the KataBankOCR kata on Coding Dojo:
 * 
 * http://codingdojo.org/cgi-bin/wiki.pl?KataBankOCR
 * 
 * By Travis Brown in response to a question by Paul Snively on the Shapeless
 * Dev mailing list:
 *
 * https://groups.google.com/d/msg/shapeless-dev/Q0VezBW2bhQ/RKF6uGljwroJ
 *
 * Tested with Scala 2.9.2 and Shapeless 1.2.3.
 */

import shapeless._, Nat._

// Evidence that the sum of (each item in L multiplied by (its distance from
// the end of the list plus one)) modulo eleven is S.
trait HasChecksum[L <: HList, S <: Nat]

implicit object hnilHasChecksum extends HasChecksum[HNil, _0]

implicit def hlistHasChecksum[
  H <: Nat,  T <: HList, S <: Nat,
  TL <: Nat, TS <: Nat,
  HL <: Nat, HS <: Nat
](implicit
  tl: LengthAux[T, TL],
  ts: HasChecksum[T, TS],
  hl: ProdAux[H, Succ[TL], HL],
  hs: SumAux[HL, TS, HS],
  sm: ModAux[HS, _11, S]
) = new HasChecksum[H :: T, S] {}

// Check that the list has nine elements and a checksum of zero.
def isValid[L <: HList](l: L)(implicit
  len: LengthAux[L, _9],
  hcs: HasChecksum[L, _0]
) {}

// Now the following valid sequence (an example from the kata) compiles:
isValid(_3 :: _4 :: _5 :: _8 :: _8 :: _2 :: _8 :: _6 :: _5 :: HNil)

// But these invalid sequences don't:
// isValid(_3 :: _1 :: _5 :: _8 :: _8 :: _2 :: _8 :: _6 :: _5 :: HNil)
// isValid(_3 :: _4 :: _5 :: _8 :: _8 :: _2 :: _8 :: _6 :: HNil)