Typelevel quicksort in Scalaで、型レベル自然数リストのコンパイル時クイックソートなるものが紹介されているので、おもしろそうだなと思って実装してみました。

こちらの記事ではshapelessのHList実装を参考に作られているのですが、今回は、色々な型の値をいくつでも入れられる型安全な“HList”を実装する - Qiitaで紹介されている HListの実装をベースに作成したものを使用しました。

細かい動作の説明を入れたり、REPLの実行例を入れたりしてたら、だいぶ長くなりそうなので分割２クールにしました。

コードはこちら( ⁰⊖⁰)
GitHub - matsu-chara/HListQuickSort: コンパイル時クイックソート

前準備

build.sbtにはdependencyにscala-reflectが指定されていますが、結果を表示する際に使用しただけなので、ソート自体には必要ありません。

また、HListってなんだ・・？( ⁰⊖⁰)という方は以前紹介したShapelessのHListでderivingをどうやるのかを学んだ話 - だいたいよくわからないブログの本題の部分を読んでいただくか、色々な型の値をいくつでも入れられる型安全な“HList”を実装する - Qiitaに詳しい説明があります。

型レベル自然数

さて、ソートを行うためにはひとまず型レベル自然数の定義必要です。ペアノの公理に従って作っていきます。

雑な説明をすると0を特別扱いで定義してしまい、1 = Succ(0), 2 = Succ(Succ(0), 3 = Succ(Succ(Succ(0))) のようにSuccをかぶせるたびに１増えた扱いします。（詳しい説明は元記事かWIkipediaで・・・）

実装

コードでは以下のようになります。

sealed trait Nat

sealed trait Zero extends Nat
case class Succ[A <: Nat](n: A) extends Nat

REPLで試してみましょう。

scala> val z = new Zero {}
z: Zero = $anon$1@6895a785

scala> val one = Succ(z)
one: Succ[Zero] = Succ($anon$1@6895a785)

scala> val two = Succ(Succ(z))
two: Succ[Succ[Zero]] = Succ(Succ($anon$1@6895a785))

いい感じにネストできていますね。

ZeroはNat型なのでSuccの引数に渡せます。また、ZeroをSuccしたoneもNat型になるため、twoのための次のSuccの引数として渡せるのがポイントです。

自然数は上記構造で以降いくらでも増やせるのですが、Succ(Succ(Succ(Succ(new Zero {}))))といちいち書くのも面倒なのでエイリアスを作ってしまいます。

object Nat {
  // types
  type _0 = Zero
  type _1 = Succ[_0]
  type _2 = Succ[_1]
  type _3 = Succ[_2]
  type _4 = Succ[_3]
  type _5 = Succ[_4]

  // values
  val _0 = new Zero {}
  val _1 = Succ(_0)
  val _2 = Succ(_1)
  val _3 = Succ(_2)
  val _4 = Succ(_3)
  val _5 = Succ(_4)

  //  次に説明するsucc,predがここに。
  // ....
}

コンパニオンオブジェクトと元のクラスの定義を分割してしまったので、REPLだとwarningがでます。一気にコピペしたい方はこちらNat.scalaから貼ってください。

REPLで試してみましょう。

scala> import Nat._
import Nat._

scala> val x : _0 = _0
x: Nat._0 = Nat$$anon$1@7ed7259e

scala> val y : _3 = _3
y: Nat._3 = Succ(Succ(Succ(Nat$$anon$1@7ed7259e)))

便利ですね。

Succと反対に数を１減らす、predも定義していましょう。

object Nat {
  // 前に書いた_0, _1, ...などがここに
  // ...

  def succ[A <: Nat](n: A): Succ[A] = Succ(n)

  def pred[A <: Nat](n: Succ[A]): A = n match {
    case Succ(m) => m
  }
}

predではパターンマッチでSuccの中身を取り出しています。 pred自体は型ではないので、対称性のためにsuccという関数を定義してみました。機能はSuccと同じです。

早速試してみましょう。

scala> import Nat._
import Nat._

// 2 + 1 == 3
scala> succ(_2)
res6: Succ[Succ[Succ[Zero]]] = 3

// 1 - 1 == 0
scala> pred(_1)
res7: Zero = 0

よさそうですね。失敗する例ではどうでしょうか？

// 1 + 1 - 1 - 1 == 0
scala> pred(pred(succ(_1)))
res11: Zero = 0

// 1 + 1 - 1 - 1 - 1 == -1(自然数ではないのでエラー)
scala> pred(pred(pred(succ(_1))))
<console>:26: error: type mismatch;
 found   : Zero
 required: Succ[?]
              pred(pred(pred(succ(_1))))

正常にエラーがでましたね。 type mismatchとなっているのに注目してください。

通常の自然数では実行時に値がマイナスになろうとしていることが発覚した段階で例外が発生し落ちるといった流れになります。しかし、今回の例ではtype error、つまりコンパイル時にエラーが検出できていることになります。

型レベル自然数の比較

型レベル自然数ができたので、大小関係を判別する機能を作っていきます。比較ができないとソートできませんからね( ⁰⊖⁰)

この部分のコードはこちらNatCompare.scala

< と <= を実装する予定ですが、まずはLess Than(<)から。

import Nat._

// expression of A < B
trait LT[A <: Nat, B <: Nat]

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

  def apply[A <: Nat, B <: Nat](implicit lt: A < B): LT[A, B] = lt
}

コードの解説の前に実行例を見てみましょう。

scala> LT(_2,_3)
<console>:25: error: too many arguments for method apply: (implicit lt: LT.<[A,B])LT[A,B] in object LT
              LT(_2,_3)

おっと、間違えました。これは値レベルの比較ではなく型レベルの比較なんでした。

scala> LT[_2, _3]
res5: LT[Nat._2,Nat._3] = LT$$anon$2@61f05988

お、なんだか出来てますね。

逆だとどうでしょうか？

scala> LT[_3, _2]
<console>:25: error: could not find implicit value for parameter lt: LT.<[Nat._3,Nat._2]
              LT[_3, _2]

なるほど _3 < _2 ではないので、implicit valueが見つからないというコンパイルエラーになっているようです。

解説

さて、ひと通り試し終えたので実装の方を見てみましょう。

まず、traitの宣言

trait LT[A <: Nat, B <: Nat]

これは読んで字のごとく A < B を表現する型になります。 Natを２つ受け取る以外は何も特別なことはないので次に進みます。

object LT {
  // 1
  type <[A <: Nat, B <: Nat] = LT[A, B]

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

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

  // 4
  def apply[A <: Nat, B <: Nat](implicit lt: A < B): LT[A, B] = lt
}

番号をふってみました。

1ではLT[A,B]のtype aliasとして <[A, B]を定義しました。こうすると A < B のような中置表現が可能になるので、大小比較のより自然な表記が可能になります。

2以降では任意の自然数と任意の自然数の間になりたつ全てのLT関係を定義しています。普通に全部書いたら大変ですが、２つのポイントに絞ると簡潔に定義することが可能です。

∀n ∈Nat に対して、 Succ[n]は0 < Succ[n]を満たす。
∀a,b ∈Natに対して a < b ならば Succ[a] < Succ[b]が成り立つ。

1つめの定義によって_0 < _1, _0 < _2... が定義されます。

2つめの定義では、すでに<が成立した関係の両辺に１足すので_1 < _2, _1 < _3...が定義されます。さらに、_1 < _2, _1 < _3の両辺に１を足すと_2 < _3, _2 < _4...になるので、以下繰り返していくと自然数全体に対して大小関係を定義したことになります。

さて、これをScalaで表現するためにはどうすればよいでしょうか。再びコードに戻って2の部分を見てみます。

2では何らかの値をimplicit defしています。

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

Bはとりあえず何らかのNatであることが（lt1の型パラメータの上限境界の指定によって）保証されています。これによって「BがNatならSucc[B] は _0 < Succ[B] を満たす」という関係を<[_0, Succ[B]]というimplicit valueを定義することで表現しています。

次に３を見てみます。

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

２の場合と同様に、A, BがNat のサブクラスであることが指定されています。さらにimplicit parameterとして A < B 型を持つltを受け取り、 Succ[A] < Succ[B] という新しい関係を定義しています。

このimplicit parameterが重要で、lt2を呼び出すコードを書いた際に、A < Bを満たすような何らかのimplicit valueが無いとコンパイルエラーになります。

ここまでくれば後は簡単で、4では A < Bという関係があったら、それを返すapply関数を定義しているだけです。

def apply[A <: Nat, B <: Nat](implicit lt: A < B): LT[A, B] = lt

以上でLTの定義は終わりです。

ちょっと横道にそれますが、ここで2と3を再び見てみます。今度はコメントをつけてみました。

  // 2
  // if true then: 0 < n
  implicit def lt1[B <: Nat] = new <[_0, Succ[B]] {}

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

2では仮定なく 0 < n という関係が定義されています。つまり if true then: 0 < nのような感じです。（コメント部分の謎言語は適当に作ったので何も実行できないしどこでも通用しません(´･_･`)）

なお、冗長になるのでコメントではB ∈ Natの部分は省略しました。この部分は型パラメータの上限境界で表現されています。

3ではimplicit parameterを通してA < Bであることが要求されています。もしA＜Bであるような関係を見つけることができたら、そこから Succ[A] < Succ[B]という新しい関係を導くことが出来ます。つまりif A < B then: Succ[A] < (Succ[B] のような感じです。

このように上限境界は∀, implicit parameterが必要なimplicit defは前提と結論のような感じに見ることができるのではないでしょうか？（実は何となくそう感じただけなのでちゃんとした知識ではありません。(´；ω；`)）

続いて Less Than Equal(<=)の定義ですが、もう解説は不要だと思います。

// expression of A <= B
trait LTEq[A <: Nat, B <: Nat]

object LTEq {
  type <=[A <: Nat, B <: Nat] = LTEq[A, B]

  // if true then: 0 <= 0
  implicit def ltEq1 = new <=[_0, _0] {}

  // if true then: 0 <= B
  implicit def ltEq2[B <: Nat] = new <=[_0, Succ[B]] {}

  // if (A <= B) then: (Succ[A] <= Succ[B])
  implicit def ltEq3[A <: Nat, B <: Nat](implicit lteq: A <= B) = new <=[Succ[A], Succ[B]] {}

  def apply[A <: Nat, B <: Nat](implicit lteq: A <= B): LTEq[A, B] = lteq

こんなかんじでLTとLTEqという大小関係が定義できました！今回は使いませんが、More Thanなんかも同じように定義できます。

来週は、これをHListに当てはめて、リストを、ある自然数より大きい数のリストと、それ以下のリストに分割するところから始めたいと思います。( ⁰⊖⁰)

だいたいよくわからないブログ

ScalaでHListを使ったコンパイル時クイックソート〜 (前編)

目次

前準備

型レベル自然数

実装

型レベル自然数の比較

解説