Skip to content

Instantly share code, notes, and snippets.

@jto
Last active December 9, 2019 07:14
  • Star 9 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save jto/2dc882c455b79378289f to your computer and use it in GitHub Desktop.
Type level quicksort
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]
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment