example of typelevel programming: merge sort by type

Main.scala

object Main extends App {

  // boilerplate
  import scala.reflect.runtime.universe._
  def show[T](value: T)(implicit tag: TypeTag[T])
    = tag.toString.replace("Main.", "")


  // type-level programming
  // Peano Arithmetic
  trait Nat
  class _0 extends Nat
  class Succ[N <: Nat] extends Nat

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


  // Comparision
  trait <[A <: Nat, B <: Nat]
  object < {
    implicit def basicLT[B <: Nat]: <[_0, Succ[B]] = new <[_0, Succ[B]] {}
    implicit def inductive[A <: Nat, B <: Nat](implicit lt: A < B)
      : Succ[A] < Succ[B] = new <[Succ[A], Succ[B]] {}

    def apply[A <: Nat, B <: Nat](implicit lt: A < B) = lt
  }
  // val comparison: _1 < _3 = <[_1, _3]
  

  trait <=[ A<: Nat, B <: Nat]
  object <= {
    implicit def basicLTE[B <: Nat]: <=[_0, B] = new <=[_0, B] {}
    implicit def inductive[A <: Nat, B <: Nat](implicit lte: A <= B)
      : Succ[A] <= Succ[B] = new <=[Succ[A], Succ[B]] {}

    def apply[A <: Nat, B <: Nat](implicit lte: A <= B) = lte
  }
  // val comparison: _1 <= _1 = <=[_1, _1]


  // Arithmetic Operations
  // add numbers as type

  /*
   * Set type parameters including Result(type)
   * But result type can be outcome from others
  trait +[A <: Nat, B <: Nat, S <: Nat]
  object + {
    implicit val zero: +[_0, _0, _0] = new +[_0, _0, _0] {}
    implicit def basicL[A <: Nat](implicit lt: _0 < A): +[A, _0, A] = new +[A, _0, A] {}
    implicit def basicR[A <: Nat](implicit lt: _0 < A): +[_0, A, A] = new +[_0, A, A] {}
    implicit def inductive[A <: Nat, B <: Nat, S <: Nat](implicit plus: +[A, B, S]) = new +[Succ[A], Succ[B], Succ[Succ[S]]] {}

    def apply[A <: Nat, B <: Nat, S <: Nat](implicit plus: +[A, B, S]) = plus
  }
  val zero: +[_0, _0, _0] = +.apply
  val two : +[_0, _2, _2] = +.apply
  val four: +[_1, _3, _4] = +.apply
  */

  trait +[A <: Nat, B <: Nat] { type Result <: Nat }
  object + {
    type Plus[A <: Nat, B <: Nat, S <: Nat] = +[A, B] { type Result = S }

    implicit val zero: Plus[_0, _0, _0] = new +[_0, _0] { type Result = _0 }
    implicit def basicL[A <: Nat](implicit lt: _0 < A): Plus[A, _0, A]
      = new +[A, _0] { type Result = A }
    implicit def basicR[A <: Nat](implicit lt: _0 < A): Plus[_0, A, A]
      = new +[_0, A] { type Result = A }
    implicit def inductive[A <: Nat, B <: Nat, S <: Nat](implicit plus: Plus[A, B, S])
      = new +[Succ[A], Succ[B]] { type Result = Succ[Succ[S]] }
    
    // def apply[A <: Nat, B <: Nat, S <: Nat](implicit plus: Plus[A, B, S]) = plus
    def apply[A <: Nat, B <: Nat](implicit plus: +[A, B])
      : Plus[A, B, plus.Result] = plus
  }
  val zero: +[_0, _0] = +.apply
  val two : +[_0, _2] = +.apply
  val four: +[_1, _3] = +.apply

  // println(show(two))
  // println(show(+.apply[_1, _3]))


  trait HList
  class HNil extends HList
  class ::[H <: Nat, T <: HList] extends HList

  trait Split[HL <: HList, L <: HList, R <: HList]
  object Split {
    implicit val basic = new Split[HNil, HNil, HNil] {}
    implicit def basic2[N <: Nat] = new Split[N :: HNil, N :: HNil, HNil] {}
    implicit def inductive[N1 <: Nat, N2 <: Nat, T <: HList, L <: HList, R <: HList]
      (implicit split: Split[T, L, R])
      = new Split[N1 :: N2 :: T, N1 :: L, N2 :: R] {}

    implicit def apply[HL <: HList, L <: HList, R <: HList]
      (implicit split: Split[HL, L, R]) = split
  }

  // val validSplit = Split.apply[_1 :: _2 :: _3 :: HNil, _1 :: _3 :: HNil, _2 :: HNil]
  // println(show(validSplit))
  
  trait Merge[LA <: HList, LB <: HList, L <: HList]
  object Merge {
    implicit def basicL[L <: HList] = new Merge[HNil, L, L] {}
    implicit def basicR[L <: HList] = new Merge[L, HNil, L] {}

    implicit def inductiveLTE[N1 <: Nat, T1 <: HList, N2 <: Nat, T2 <: HList, IR <: HList]
      (implicit merge: Merge[T1, N2 :: T2, IR], lte: N1 <= N2)
      = new Merge[N1 :: T1, N2 :: T2, N1 :: IR] {}

    implicit def inductiveGT[N1 <: Nat, T1 <: HList, N2 <: Nat, T2 <: HList, IR <: HList]
      (implicit merge: Merge[N1 :: T1, T2, IR], lte: N2 < N1)
      = new Merge[N1 :: T1, N2 :: T2, N2 :: IR] {}


    def apply[LA <: HList, LB <: HList, L <: HList](implicit merge: Merge[LA, LB, L])
      = merge

  }

  // val validMerge = Merge.apply[_1 :: _3 :: HNil, _2 :: _4 :: HNil, _1 :: _2 :: _3 :: _4 :: HNil]
  // println(show(validMerge))


  /*
  trait Sort[L <: HList, O <: HList]
  object Sort {
    implicit val basicNil = new Sort[HNil, HNil] {}
    implicit def basicOne[N <: Nat] = new Sort[N :: HNil, N :: HNil] {}

    implicit def inductive[I <: HList, L <: HList, R <: HList, SL <: HList, SR <: HList, O <: HList]
      (implicit
        split: Split[I, L, R],
        sortL: Sort[L, SL],
        sortR: Sort[R, SR],
        merge: Merge[SL, SR, O]
      ) = new Sort[I, O] {}
     
    def apply[L <: HList, O <: HList](implicit sort: Sort[L, O]) = sort
  }

  // val validSort = Sort.apply[_4 :: _3 :: _5 :: _1 :: _2 :: HNil, _1 :: _2 :: _3:: _4 :: _5 :: HNil]
  // println(show(validSort))
  */

  trait Sort[L <: HList] { type Result <: HList }
  object Sort {
    type SortOp[L <: HList, O <: HList] = Sort[L] { type Result = O }
    implicit val basicNil = new Sort[HNil] { type Result = HNil }
    implicit def basicOne[N <: Nat] = new Sort[N :: HNil] { type Result = N :: HNil }

    implicit def inductive[I <: HList, L <: HList, R <: HList, SL <: HList, SR <: HList, O <: HList]
      (implicit
        split: Split[I, L, R],
        sortL: SortOp[L, SL],
        sortR: SortOp[R, SR],
        merge: Merge[SL, SR, O]
      ) = new Sort[I] { type Result = O }
     
    // def apply[L <: HList](implicit sort: Sort[L]): SortOp = sort
    def apply[L <: HList](implicit sort: Sort[L]): SortOp[L, sort.Result] = sort
  }

  val validSort: Sort[_4 :: _3 :: _5 :: _1 :: _2 :: HNil] = Sort.apply
  println(show(validSort))
  println(show(Sort.apply[_4 :: _3 :: _5 :: _1 :: _2 :: HNil]))

}

Playlist https://www.youtube.com/playlist?list=PLmtsMNDRU0ByOQoz6lnihh6CtMrErNax7
Post https://blog.rockthejvm.com/type-level-programming-part-1/