Implementing a type-level collapsible function

Collapsible.scala

/**
 * For type-level calculations, it might help to think of a prolog implementation
 * of `collapse`. We inline the use of `splitAt` and `reduceLeft`, for saving
 * some lines
 *
 *   // it is true that collapsing a list with no ints gives the list back as remainder
 *   collapse(ls, nil, op, nil, ls).
 *
 *   // we can collapse a list for a given `Nat n`, if we can split the input
 *   // list, reduce the prefix (over the `op` operator), recursively collapse the
 *   // suffix, and then concatenate everything
 *
 *   collapse(ls, n :: ns, op, col :: res, rem) :-
 *     split(ls, n, pre, suf),
 *     reduce(pre, op, col),
 *     collapse(suf, ns, res, rem).
 */
import shapeless._
import ops.hlist._


/**
 * Let's create some proofs that stuff is collapsible
 * The Collapsible trait will be the interface. The underlying proof,
 * as seen in the prolog implementation will have 4 parameters, and will
 * be known as `Collapsible0`. This is in line with the design of stuff
 * in shapeless
 */
trait Collapsible[L <: HList, NatL <: HList, Op <: Poly] {
  /**
   * The result type of this collapsible list
   */
  type Out
    /**
   * the apply function, that will collapse the list
   */
  def apply(ls: L, ns: NatL, op: Op): Out
}

/**
 * a companion object for Collapsible
 */
object Collapsible {

  /**
   * An auxiliary type that gives us the return type as a parameter too, a la shapeless
   */
  type Aux[L <: HList, NatL <: HList, Op <: Poly, Res] = Collapsible[L, NatL, Op] {
    type Out = Res
  }

  /**
   * given proof of collapsibility, we can apply it
   * the proof is implicit, which is the means in Scala to perform search for
   * the right proof.
   */
  def apply[L <: HList, NatL <: HList, Op <: Poly]
           (implicit collapsible: Collapsible[L, NatL, Op]): Aux[L, NatL, Op, collapsible.Out]
    = collapsible

  /**
   * The term-level computation. Recall the prolog implementation above:
   * We need proof that a list of elements is collapsible, and gives us some result
   * as well as a remaining list. Hence we need proof of a `Collapsible0`.
   */
  implicit def collapse[
      L <: HList,
      NatL <: HList,
      Op <: Poly,
      ResultL <: HList,
      Remaining <: HList](
      implicit collapsible0: Collapsible0[L, NatL, Op, ResultL, Remaining]
      ): Aux[L, NatL, Op, (ResultL, Remaining)] =
    new Collapsible[L, NatL, Op] {
      type Out = (ResultL, Remaining)
      def apply(ls: L, ns: NatL) = collapsible0(ls, ns)
    }

  /**
   * Collapsible0 is a type representing the complete proof for
   * collapsibility. Inspired by shapeless' `Split0`
   */

  trait Collapsible0[L <: HList, NatL <: HList, Op <: Poly,
                     ResultL <: HList, Remaining <: HList] {
    def apply(ls: L, ns: NatL, op: Op): (ResultL, Remaining)
  }

  /**
   * takes care of the case where an empty list of nats is provided
   * i.e. it is true that collapsing with a empty list of nats just returns
   * the original list as a remainder
   */
  implicit def collapseEmptyList[L <: HList, Op <: Poly] =
    new Collapsible0[L, HNil, Op, HNil, L] {
      def apply(ls: L, ns: HNil) = (HNil, ls)
    }

  /**
   * The recursive collapse
   */
  implicit def collapseRec[
      L <: HList,
      N <: Nat, NS <: HList,
      Op <: Poly,
      Col1, CollapseRest <: HList,
      Pre <: HList, Rem <: HList,
      Remaining <: HList](
      implicit splittable: Split.Aux[L, N, Pre, Rem],
               reducible: RightReducer.Aux[Pre, Op, Col1],
               recCollapse: Collapsible0[Rem, NS, Op, CollapseRest, Remaining]
      ): Collapsible0[L, N :: NS, Op, Col1 :: CollapseRest, Remaining] =

    new Collapsible0[L, N :: NS, Op, Col1 :: CollapseRest, Remaining] {

      def apply(ls: L, ns: N :: NS) = {
        /**
         * collapsing the first part of the list only
         */
        val (pre, collapse1Rest) = ls.split[N]
        val collapse1 = reducible(pre) //COMPILES NOW, YAY

        val (collapseRest, remainingN) = recCollapse(collapse1Rest, ns.tail)
        (collapse1 :: collapseRest, remainingN)
      }
    }
  
    /**
     * a typecheck test
     */
    object listCollapser extends Poly {
      implicit def list1lit2[A, B] = use((ls1: List[A], ls2: List[B]) => ls1 ++ ls2)
    }

    import shapeless.Nat._
    type PList[A, B, C] = List[A] :: List[B] :: List[C] :: HNil
    def collapseTest[A, B, C](ls: PList[A, B, C])
                             (implicit collapsible: Collapsible.Aux[PList[A, B, C],
                               _2 :: HNil,
                               listCollapser.type,
                               (List[Any] :: HNil, List[C] :: HNil)]) =
      collapsible(ls, _2 :: HNil)
}