seoh · July 18, 2021 16:11 · Jul 18, 2021 · Aug 31, 2020
diff --git a/Main.scala b/Main.scala
@@ -0,0 +1,175 @@
+
+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]))
+
+}