Solving the Tower of Hanoi at the type level

tower-of-hanoi.scala

/**
* Type-level Tower of Hanoi
* by Travis Brown
*
* Note: not optimal, and probably won't work for some valid inputs.
* Tested with Scala 2.9.2 and Shapeless 1.2.3.
*/

import shapeless._, Nat._

trait Increasing[L <: HList]
implicit object hnilIncreasing extends Increasing[HNil]
implicit def hlistIncreasing1[N <: Nat] = new Increasing[N :: HNil] {}
implicit def hlistIncreasing2[M <: Nat, N <: Nat, T <: HList](implicit
  lt: LT[M, N],
  in: Increasing[N :: T]
) = new Increasing[M :: N :: T] {}

sealed trait Solvable[A <: HList, B <: HList, C <: HList] {
  def show: String
}

object Complete extends Solvable[HNil, HNil, _1 :: _2 :: _3 :: HNil] {
  def show = "COMPLETE"
}

case class Step[
   A <: HList, B <: HList, C <: HList,
  SA <: HList, SB <: HList, SC <: HList
](next: Solvable[SA, SB, SC], step: String) extends Solvable[A, B, C] {
  def show = step + "\n" + next.show
}

trait AC {
  implicit def stepAC[AH <: Nat, AT <: HList, B <: HList, C <: HList](implicit
    i: Increasing[AH :: C], j: Increasing[AH :: AT], s: Solvable[AH :: AT, B, C]
  ) = Step[AT, B, AH :: C, AH :: AT, B, C](s, "C to A")
}

trait AB extends AC {
  implicit def stepAB[AH <: Nat, AT <: HList, B <: HList, C <: HList](implicit
    i: Increasing[AH :: B], j: Increasing[AH :: AT], s: Solvable[AH :: AT, B, C]
  ) = Step[AT, AH :: B, C, AH :: AT, B, C](s, "B to A")
}

trait BC extends AB {
  implicit def stepBC[A <: HList, BH <: Nat, BT <: HList, C <: HList](implicit
    i: Increasing[BH :: C], j: Increasing[BH :: BT], s: Solvable[A, BH :: BT, C]
  ) = Step[A, BT, BH :: C, A, BH :: BT, C](s, "C to B")
}

trait BA extends BC {
  implicit def stepBA[A <: HList, BH <: Nat, BT <: HList, C <: HList](implicit
    i: Increasing[BH :: A], j: Increasing[BH :: BT], s: Solvable[A, BH :: BT, C]
  ) = Step[BH :: A, BT, C, A, BH :: BT, C](s, "A to B")
}

trait CB extends BA {
  implicit def stepCB[A <: HList, B <: HList, CH <: Nat, CT <: HList](implicit
    i: Increasing[CH :: B], j: Increasing[CH :: CT], s: Solvable[A, B, CH :: CT]
  ) = Step[A, CH :: B, CT, A, B, CH :: CT](s, "B to C")
}

trait CA extends CB {
  implicit def stepCA[A <: HList, B <: HList, CH <: Nat, CT <: HList](implicit
    i: Increasing[CH :: A], j: Increasing[CH :: CT], s: Solvable[A, B, CH :: CT]
  ) = Step[CH :: A, B, CT, A, B, CH :: CT](s, "A to C")
}

object All extends CA {
  implicit val complete = Complete
}

import All._

// scala> implicitly[Solvable[_1 :: _2 :: _3 :: HNil, HNil, HNil]].show
// res0: String =
// A to C
// A to B
// C to B
// A to C
// B to C
// C to B
// B to A
// A to C
// B to A
// C to B
// A to C
// B to C
// COMPLETE

That is outstanding.