Typelevel quicksort article

0_qs.scala

sealed trait Nat

10_qs.scala

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]] {}
}

11_qs.scala

implicit def lt1[B <: Nat] = new <[_0, Succ[B]] {}

12_qs.scala

:t LT[_0, _1]
LT[_0, _1]

13_qs.scala

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

14_qs.scala

:t LT[_1, _2]
LT[_1, _2]
// 1 < 2

:t LT[_2, _1]
<console>:16: error: could not find implicit value for parameter lt: LT.<[_2, _1]
              LT[_2, _1]

15_qs.scala

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]] {}
}

16_qs.scala

sealed abstract class List[+A]
case object Nil extends List[Nothing]
final case class ::[B](head: B, tail: List[B]) extends List[B]

17_qs.scala

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

18_qs.scala

type NS = _1 :: _0 :: _3 :: _2 :: HNil

19_qs.scala

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

1_qs.scala

final class _0 extends Nat

20_qs.scala

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

21_qs.scala

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 }

22_qs.scala

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 }

23_qs.scala

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

24_qs.scala

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 }
}

25_qs.scala

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

26_qs.scala

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
      }
}

27_qs.scala

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

28_qs.scala

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

29_qs.scala

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

2_qs.scala

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

30_qs.scala

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
    }

31_qs.scala

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

3_qs.scala

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

4_qs.scala

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 }
}

5_qs.scala

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

6_qs.scala

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

7_qs.scala

:t Sum[_0, Succ[_0]]
Sum.Aux[_0, Succ[_0], Succ[_0]] // 0 + 1 = 1

8_qs.scala

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 }

9_qs.scala

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