Type level quicksort

qs.scala

object jto {

  type _1 = Succ[_0]
  type _2 = Succ[_1]
  type _3 = Succ[_2]
  type _4 = Succ[_3]
  type _5 = Succ[_4]

  // Natural numbers (extracted from shapeless)

  sealed trait Nat
  final class Succ[P <: Nat]() extends Nat
  final class _0 extends Nat

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

  object Sum {
    def apply[A <: Nat, B <: Nat](implicit sum: Sum[A, B]): Aux[A, B, sum.Out] = sum

    type Aux[A <: Nat, B <: Nat, C <: Nat] = Sum[A, B] { type Out = C }

    implicit def sum1[B <: Nat]: Aux[_0, B, B] = new Sum[_0, B] { type Out = B }

    implicit def sum2[A <: Nat, B <: Nat]
      (implicit sum : Sum[A, Succ[B]]): Aux[Succ[A], B, sum.Out] = new Sum[Succ[A], B] { type Out = sum.Out }
  }

  // Sum Demo

  // :t Sum[_0, Succ[_0]]
  // Sum.Aux[_0, Succ[_0], Succ[_0]]

  // :t Sum[Succ[_0], Succ[Succ[_0]]]
  // Sum.Aux[Succ[_0], Succ[Succ[_0]], Succ[Succ[Succ[_0]]]]
  // We can show that 1 + 3 = 3 + 1

  // Taken from shapeless

  trait LTEq[A <: Nat, B <: Nat]
  object LTEq {
    def apply[A <: Nat, B <: Nat](implicit lteq: A <= B): LTEq[A, B] = lteq

    type <=[A <: Nat, B <: Nat] = LTEq[A, B]

    implicit def ltEq1 = new <=[_0, _0] {}
    implicit def ltEq2[B <: Nat] = new <=[_0, Succ[B]] {}
    implicit def ltEq3[A <: Nat, B <: Nat](implicit lteq : A <= B) = new <=[Succ[A], Succ[B]] {}
  }

  trait LT[A <: Nat, B <: Nat]
  object LT {
    def apply[A <: Nat, B <: Nat](implicit lt: A < B): LT[A, B] = lt

    type <[A <: Nat, B <: Nat] = LT[A, B]

    implicit def lt1[B <: Nat] = new <[_0, Succ[B]] {}
    implicit def lt2[A <: Nat, B <: Nat](implicit lt : A < B) = new <[Succ[A], Succ[B]] {}
  }

  // Hlist (extracted from shapeless)

  sealed trait HList

  final class ::[+H, +T <: HList] extends HList

  class HNil extends HList

  trait LTEqs[H <: HList, A <: Nat] {
    type Out <: HList
  }

  object LTEqs {
    import LT._
    import LTEq._

    type Aux[H <: HList, A <: Nat, Out0 <: HList] = LTEqs[H, A] { type Out = Out0 }

    def apply[H <: HList, A <: Nat](implicit lts: LTEqs[H, A]): Aux[H, A, lts.Out] = lts

    implicit def hnilLTEqs[A <: Nat]: Aux[HNil, A, HNil] = new LTEqs[HNil, A] { type Out = HNil }

    implicit def hlistLTEqsLower[A <: Nat, H <: Nat, T <: HList](implicit lts : LTEqs[T, A], l: H <= A): Aux[H :: T, A, H :: lts.Out] =
      new LTEqs[H :: T, A] { type Out = H :: lts.Out }

    implicit def hlistLTEqsGreater[A <: Nat, H <: Nat, T <: HList](implicit lts : LTEqs[T, A], l: A < H): Aux[H :: T, A, lts.Out] =
      new LTEqs[H :: T, A] { type Out = lts.Out }
  }

  // val _0 = new _0()
  // :t LTEqs[_1 :: _0 :: _3 :: _2 :: HNil, _2]
  // LTEqs.Aux[_1 :: _0 :: _3 :: _2 :: HNil, _2, _1 :: _0 :: _2 : HNil]

  trait GTs[H <: HList, A <: Nat] {
    type Out <: HList
  }

  object GTs {
    import LT._
    import LTEq._

    type Aux[H <: HList, A <: Nat, Out0 <: HList] = GTs[H, A] { type Out = Out0 }

    def apply[H <: HList, A <: Nat](implicit lts: GTs[H, A]): Aux[H, A, lts.Out] = lts

    implicit def hnilGTEqs[A <: Nat]: Aux[HNil, A, HNil] = new GTs[HNil, A] { type Out = HNil }

    implicit def hlistGTEqsLower[A <: Nat, H <: Nat, T <: HList](implicit lts : GTs[T, A], l: A < H): Aux[H :: T, A, H :: lts.Out] =
      new GTs[H :: T, A] { type Out = H :: lts.Out }

    implicit def hlistGTEqsGreater[A <: Nat, H <: Nat, T <: HList](implicit lts : GTs[T, A], l: H <= A): Aux[H :: T, A, lts.Out] =
      new GTs[H :: T, A] { type Out = lts.Out }
  }

  // :t GTs[_1 :: _0 :: _3 :: _2 :: HNil, _2]
  // GTs.Aux[_1 :: _0 :: _3 :: _2 :: HNil, _2, _3 :: HNil]

  trait Prepend[P <: HList, S <: HList] { type Out <: HList }

  object Prepend {
    type Aux[P <: HList, S <: HList, Out0 <: HList] = Prepend[P, S] { type Out = Out0 }

    def apply[P <: HList, S <: HList](implicit prepend: Prepend[P, S]): Aux[P, S, prepend.Out] = prepend

    implicit def hnilPrepend1[P <: HNil, S <: HList]: Aux[P, S, S] =
      new Prepend[P, S] {
        type Out = S
      }

    implicit def hlistPrepend[PH, PT <: HList, S <: HList]
      (implicit pt : Prepend[PT, S]): Aux[PH :: PT, S, PH :: pt.Out] =
        new Prepend[PH :: PT, S] {
          type Out = PH :: pt.Out
        }
  }

  trait Sorted[L <: HList] {
    type Out <: HList
  }

  object Sorted {
    def apply[L <: HList](implicit sorted: Sorted[L]): Aux[L, sorted.Out] = sorted

    type Aux[L <: HList, Out0 <: HList] = Sorted[L] { type Out = Out0 }

    implicit def hnilSorted: Aux[HNil, HNil] = new Sorted[HNil] { type Out = HNil }

    implicit def hlistSorted[H <: Nat, T <: HList, lsOut <: HList, gsOut <: HList, smOut <: HList, slOut <: HList]
      (implicit
        ls: LTEqs.Aux[T, H, lsOut],
        gs: GTs.Aux[T, H, gsOut],
        sortedSmaller: Sorted.Aux[lsOut, smOut],
        sortedLarger: Sorted.Aux[gsOut, slOut],
        preps: Prepend[smOut, H :: slOut]
      ): Aux[H :: T, preps.Out] =
        new Sorted[H :: T] {
          type Out = preps.Out
        }
  }

  // :t Sorted[_1 :: _0 :: _3 :: _2 :: HNil]
  // Sorted.Aux[_1 :: _0 :: _3 :: _2 :: HNil, _0 :: _1 :: _2 :: _3 :: HNil]

}