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

自然数

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

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

ペアノの公理

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

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

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

ここで示した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つの自然数 A と B を受け取り、別の自然数 Out を返します。この型レベル関数の作成に使われているのが 依存型 です。 Out 型は A と B に依存しています。つまり、Scalaに A と B を与えれば、何が 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が A と B とするなら、 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 も空であるか、もしくは head と tail があるかのいずれかです。どちらのリストも定義が非常によく似ているのが分かりますね。本来は、 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 をソートし、その結果できた HList を smOut とします。
• Sorted.Aux[gsOut, slOut] ⇒ gsOut をソートし、その結果できた HList を slOut とします。

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. 私たちはクイックソートをやっとのことで実装しましたが、とても時間がかかったので、人の手でソートしたほうがずっと早いかもしれません。