Skip to content

Instantly share code, notes, and snippets.

@jto jto/qs.scala
Last active Dec 5, 2016

Embed
What would you like to do?
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
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.