Scalaで型レベル”だけ”でクイックソート

Scalaの型システムが先進的であることは、皆さんもご存じのことかと思います。この投稿では、Scalaの型システムのみを使ったクイックソートアルゴリズムの実装方法をご紹介したいと思います。なお、ここで紹介するデモの完全なコードはこちらをご覧ください。

自然数

まずは準備から。ソートアルゴリズムを実装するには、ソートする対象が必要ですよね。ここでは自然数を用います。もちろん、Scalaの型システムには利用可能な自然数はありません。そんなわけで、全ての自然数の型を作る必要があります。

型を無限に作るというのは、恐らく時間の浪費になるでしょうから、ここはもう少し賢い手を考えます。そう、数学を使いましょう。

ペアノの公理

ペアノの公理とは、自然数を形式的に定義するためのシンプルな方法のことです。

  • 0は特別なものとする。0は自然数である。
  • 全ての自然数nには、それに続くもう1つ別の自然数S(n)が存在する。
  • 0はいかなる自然数にも続くものではない。その他の全ての自然数には後続の自然数が存在する。
  • 異なる自然数が、同じ後続の自然数を持つことはない。
  • 自然数は、等式で比較できる。等式は反射的であり、対称的であり、推移的である。
  • ある命題Pにおいて、以下の条件を満たせばPは全ての自然数に対して真である。
    • P0について真である。
    • Pが数字nに対して真の時(P(n)は真なり)、Pnの後続に対して真である(P(S(n))は真なり)。

ペアノの計算法についてより詳しく知りたい方はWikipediaをご覧ください。

これらの公理を頭に入れておくと、Scalaの型システムで自然数を表現するのが簡単になります。

まずはNatトレイトを作成してみましょう。

sealed trait Nat

0は特別なものとする。0は自然数である。(0は無効な型名なので、_0とします)。

final class _0 extends Nat

全ての自然数nには、それに続くもう1つ別の自然数S(n)が存在する。

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

これらのクラスを定義すれば、どんな自然数も表現できるようになります。早速1から5までの自然数を定義してみましょう。

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

簡単ですよね。

基本の計算

これらの数字が実際に利用可能かを証明するため、足し算の実装をします。ここで再び、ペアノを参照することにしましょう(画像はWikipediaより)。

Peano's sum

分かりにくいかもしれませんが、これで十分です。幸い、ほとんどこのまま型に変換します。

ここで示したScalaでの変換は、私が臆面もなくshapelessから取ってきたものです。以降、説明に必要なものがshapelessに存在している場合は、そこから取ってくることにします。「偉大な芸術家は盗む」って言いますよね(それに私は怠け者ですし)。もちろん、参考したところについては逐一言及します。それから、より明快にするため、関係ないと思われる一部のコードを削除する場合はあります。

それでは、以下がshapelessのSumです。

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

この素晴らしさに少し圧倒されているのでないでしょうか。まずはゆっくりと深呼吸し、1つずつ見ていきましょう。

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

Sumは2つの自然数ABを受け取り、別の自然数Outを返します。この型レベル関数の作成に使われているのが依存型です。Out型はABに依存しています。つまり、ScalaにABを与えれば、何がOutかを魔法のように算出するというわけです。

これで足し算の表現方法が分かりましたね。A + B = Outです。

表現まではできたので、次は実際に2つの自然数を足した結果を算出してみましょう。

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

任意の自然数bに対し、0 + b = bというのが、私たちの定義する足し算の基本ケースです。

applyメソッドを用いて、このケースをテストしてみましょう。

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

その他のケースは帰納法により定義されます。

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 }

これの示すところは、2つのNatがABとするなら、S(A) + B = A + S(B)であるということです。

これはWikipediaで定義されている公理とは異なりますが、以下の理由から同等と言えます。

  • A + S(B) = S(A + B)
  • 同様にS(A) + B = S(A + B)
  • 故にA + S(B) = S(A + B) = S(A) + Bである。

そこで、暗黙の解決によって3 + 1の足し算を評価しようとすると、Scalaのコンパイラは次のステップを踏むことになります。

  1. S(S(S(0))) + S(0) = S(S(0)) + S(S(0))
  2. S(S(0)) + S(S(0)) = S(0) + S(S(S(0)))
  3. S(0) + S(S(S(0))) = 0 + S(S(S(S(0))))
  4. 基本ケースに戻り0 + S(S(S(S(0)))) = S(S(S(S(0))))
  5. 故にS(S(S(0))) + S(0) = S(S(S(S(0))))である。

ScalaのREPLでテストしてみましょう。

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

型システムで基本的な計算ができますね。

不等式

クイックソートを実装するには、自然数を比較できるようになる必要があります。ここで再び、shapelessが役に立ちました。

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

先ほどのように、基本となるケースである、0だけをカバーし、帰納的に他の全ケースに当てはめます。ゼロは最小の自然数なので、∀x∈N. 0 < S(x)となります。

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

すぐにテストしてみます。

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

ご存知のように、型は命題であり、プログラムは証明です。型LT[_0, _1]という値があるので、コンパイラは0 < 1であることを証明しただけです(Curry-Howard対応をご覧ください)。

他の場合は全て、∀ x,y ∈ N. S(x) < S(y) ⇔ x < yのように、先行する数字を単に比較するだけです。

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

再度、コンパイラは基本となるケースへのステップをたどります。

  1. S(S(0)) < S(S(S(0))) ⇔ S(0) < S(S(0))
  2. S(0) < S(S(0)) ⇔ 0 < S(0)
  3. 基本のケースに戻る

では、テストしてみましょう。

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]] {}
}
  • インスタンスLT[_1, _2]が存在すれば、1 < 2を証明できることを意味する
  • インスタンスLT[_2, _1]が存在しなければ、2 < 1を証明できないことを意味する

クイックソートを実装するには、も使用します。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]] {}
}

型レベルのリスト、すなわちHList

さて、ここまで、自然数の扱い方を見てきましたが、ソートするには、自然数のリストも必要になりますね。しかし、リストはどのように機能するのでしょうか。以下は、Scalaのリストを簡素化したものです。

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

リストは再帰的に定義され、次の2つの状態になり得ます。

  • 空のリスト
  • 同じ型の、最初の要素(head)と他のリスト(tail

リストの型を表すために、HListを使います。HListは、型システムに反復が生じない限り、全く同じように定義されます。繰り返しになりますが、HListはshapeless内で既に定義されています。

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

従来のリストのように、HListも空であるか、もしくはheadtailがあるかのいずれかです。どちらのリストも定義が非常によく似ているのが分かりますね。本来は、HListも値を格納するリストです。今は、型システムの話をしているので、はっきりと分かるように不要なコードを削除しました。

それでは、自然数の型レベルリストを作成してみましょう。

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

パーティション操作

必要なものはほとんど準備できました。まずはパーティションを作成し、HListを3つの要素に分割しなければなりません。

  • ピボット
  • ピボットと等しいか小さい型のHList
  • ピボットより大きい型のHList

今回は、shapelessからはビルトインは提供されていないので、自力で対処します。

小さい要素を見つけ出すことから始めましょう。与えられたリストHと、自然数Aがあります。ここから、新しいHlistを作成したいと思います。

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

では、解決策の実装を始めましょう。先ほどのように、基本となるケース、つまり空のリストから始めます。

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

ここで”他にはどんなケースがあるのか”と、考えてみる必要があります。リストを使った関数の機能を決める際に、通常、最初の要素(head)でパターンマッチを行い、それをtailまで、再帰的に呼び出します。

やることは、それだけです。その場合、2つのケースが考えられます。最初の要素がピボットより小さいかピボットと等しい場合は、維持します。

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 }

コードをテストしてみます。

: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]

HListの連結

ゴールはもうすぐです。クイックソードのアルゴリズムでは、リストの連結が必要です。Hlistの先頭に、別のHlistを追加する方法を実装しなければなりません。ここまでの過程で、自分で方法を見つけられるくらいに十分に内容を理解されていると思います。

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

テストしてみます。

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

ソート

ついに最終段階です。クイックソートの実装に必要なものはすべてそろいました。あとは、それらを統合するだけです。

ソートのアルゴリズムは、リストを与えると、リストを返します。

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

先ほどと同じように、最初は基本となるケースを扱います。空のリストをソートすると、空のリストが返されます。

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
    }

おっと、今回はかなりたくさんの型がありますね。ありがたいことに、それほど難しくはありません。

  1. 最初に、ピボットを抽出します。簡潔にするために、単純に、リストのheadであるHとtailであるTを抽出します。new Sorted[H :: T] { ... }となります。
  2. その後、tailのTを、2つのサブリストに分割します。コンパイラに、以下のことを判別するように要求します(暗黙の引数を使います)。

  • LTEqs.Aux[T, H, lsOut]Tの中から、Hと等しいかそれより小さい全ての型を取得します。このサブリストをlsOutとします。
  • GTs.Aux[T, H, gsOut], Tの中から、Hより大きい全ての型を取得します。このサブリストをgsOutとします。

3. サブリストをソートします。

  • Sorted.Aux[lsOut, smOut]lsOutをソートし、その結果できたHListsmOutとします。
  • Sorted.Aux[gsOut, slOut]gsOutをソートし、その結果できたHListslOutとします。

4. 小さい型のソートしたリストとピボット、そして大きい型のソートしたリストを連結します。

  • Prepend[smOut, H :: slOut]

これで終了です。結果は、preps.Outです。

最後のテストをしてみましょう。

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

結論

  1. このように優れたものを、実際に使われているメインストリームの言語に実装できるということは、テンプレートが少々必要であるとしても、実に素晴らしいことです。
  2. 私たちはクイックソートをやっとのことで実装しましたが、とても時間がかかったので、人の手でソートしたほうがずっと早いかもしれません。