Effective ATS: マージソート

この記事では、改良に基づく (refinement-based) プログラミングスタイルを示す具体的な例としてマージソートを作ってみようと思います。

マージソートとは何ですか？

マージソートに仕様的な実装を与えることで、この疑問に答えさせてください。 [mergesort] が呼び出されるデータを表わす型 [myseq] が次のように宣言されていると仮定します:

abstype myseq

[mergesort] に次のインターフェイスを割り当てるのは自然です:

fun mergesort (xs: myseq): myseq

[mergesort] の素直な実装は次のようになるでしょう:

implement
mergesort (xs) = let
  val n = myseq_length (xs)
in
//
  if n >= 2 then let
    val (xs1, xs2) = myseq_split (xs)
  in
    myseq_merge (mergesort (xs1), mergesort (xs2))
  end else (xs) // end of [if]
//
end // end of [mergesort]

このとき、関数 [myseq_length], [myseq_split], [myseq_merge] には次の型が割り当てられています:

fun myseq_length (xs: myseq): int
fun myseq_split (xs: myseq): (myseq, myseq)
fun myseq_merge (xs1: myseq, xs2: myseq): myseq

これらの機能は次のように要約できます:

[myseq_length] は与えられた myseq 値の長さを返します。
[myseq_split] は与えられた myseq 値を2つの myseq 値に分割します。
[myseq_merge] は与えられた2つのソート済み myseq 値を1つのソート済み myseq 値にマージします。

ATS の構文に不慣れな読者を考えても、おそらく上記の [mergesort] の仕様的な実装は英語や他の自然言語でマージソートを表現するより好ましいと主張できるでしょう。

依存型を使った仕様記述

マージソートの実装が再帰的なら、実装された関数 [mergesort] の終了を予想できる理由が必要です。 [mergesort] の終了について議論するなら、必然的に myseq 値の長さについて考えなければなりません。この myseq 値の長さとは、その myseq 値が表現する数列に含まれる要素の数になります。

ATS では、次のように [myseq] を作る型コンストラクタに整数パラメータを1つ渡して、型を改良することができます:

abstype myseq(n:int)

静的な整数 N が与えられたとき、[myseq(N)] は長さ N の myseq 値を表わします。与えられた myseq 値とそのソート済みの値は同じ長さを持つという不変条件を捕捉するために、[mergesort] に割り当てられた型を次のように改良できます:

fun mergesort{n:nat} (xs: myseq(n)): myseq(n)

関数 [myseq_length], [myseq_split], [myseq_merge] には、次のようなより豊富な情報を含んだ型を割り当てることができます:

//
fun myseq_length{n:int} (xs: myseq(n)): int(n)
//
fun myseq_split{n:int | n >= 2}
  (xs: myseq(n)): [n1,n2:pos | n1+n2==n] (myseq(n1), myseq(n2))
//
fun myseq_merge{n1,n2:nat} (xs1: myseq(n1), xs2: myseq(n2)): myseq(n1+n2)
//

[myseq_split] に割り当てられた型は、この関数が少なくとも2個以上の要素を含む myseq 値のみに適用することができ、それが返す2つの myseq 値は与えられた myseq 値よりも厳密に小さくなることを意味していることに注意してください。

上記の [mergesort] の実装は次のバージョンのように若干修正できます:

implement
mergesort (xs) = let
//
fun sort
  {n:nat} .<n>.
(
  xs: myseq(n)
) : myseq(n) = let
  val n = myseq_length (xs)
in
  if n >= 2 then let
    val (xs1, xs2) = myseq_split (xs)
  in
    myseq_merge (sort (xs1), sort (xs2))
  end else (xs) // end of [if]
end // end of [sort]
//
in
  sort (xs)
end // end of [mergesort]

[sort] は (プログラマによって与えられた) 停止性メトリクス (termination metric) <n> に基づいて停止することが証明されていることに注意してください。

[myseq_split] を実装するなら、次のインターフェイスが適切であるとすぐに気が付くでしょう:

fun myseq_split{n:int | n >= 2}
  (xs: myseq(n), n: int n): (myseq(n/2), myseq(n-n/2))

このインターフェイスは、[myseq_split] が長さ n の myseq 値と値 n の整数に適用されると、長さ n/2 と n-n/2 の myseq 値のペアを返すことを提示しています。これで [mergesort] の実装は次のように若干修正できます:

implement
mergesort (xs) = let
//
fun sort
  {n:nat} .<n>.
(
  xs: myseq(n), n: int n
) : myseq(n) = let
in
  if n >= 2 then let
    val n2 = half (n)
    val (xs1, xs2) = myseq_split (xs, n)
  in
    myseq_merge (sort (xs1, n2), sort (xs2, n-n2))
  end else (xs) // end of [if]
end // end of [sort]
//
in
  sort (xs, myseq_length(xs))
end // end of [mergesort]

これで型検査できるマージソートの仕様的な実装が手に入りました。この実装は、リストや配列のような具体的な型のマージソートを実装するための青写真として考えることができます。

リストのマージソート

予想されることですが、リストに対するマージソートのインターフェイスは次のように与えられます:

fun{a:t0p}
mergesort{n:nat} (xs: list (a, n)): list (a, n)

このインターフェイスは、[mergesort] がその引数として与えられたリスト中の要素の型をパラメータ化した関数テンプレートであることを示しています。ここでは [myseq_merge] に注目しましょう。この関数には次のようなインターフェイスを割り当てられます:

fun{a:t0p}
myseq_merge
  {n1,n2:nat}
  (xs1: list(a, n1), xs2: list(a, n2)): list(a, n1+n2)
// end of [myseq_merge]

次のように、リストに対する [myseq_merge] は素直に実装できます:

implement
{a}(*tmp*)
myseq_merge
  (xs10, xs20) = let
in
//
case+ xs10 of
| cons (x1, xs11) =>
  (
    case+ xs20 of
    | cons (x2, xs21) => let
        val sgn = gcompare_val<a> (x1, x2)
      in
        if sgn <= 0
          then cons{a}(x1, myseq_merge<a> (xs11, xs20))
          else cons{a}(x2, myseq_merge<a> (xs10, xs21))
        // end of [if]
      end (* end of [cons] *)
    | nil ((*void*)) => xs10
  )
| nil ((*void*)) => xs20
//
end // end of [myseq_merge]

[gcompare_val] は値を比較する総称関数テンプレートであることに注意してください。

リストのマージソートの実装全体と追加のテストコードは mergesort_list.dats から入手できます。

配列のマージソート

上記での [mergesort] の抽象的な仕様的実装はいわゆる関数型スタイルです。先の実装は (命令型スタイルの) 配列に対するマージソートを実装するのに適合しません。そこで、この主張のために試しにやってみましょう。

まずはじめに、ATS における配列はC言語スタイルなので、その配列にはサイズ情報が付属していません。そこで、[mergesort] のインターフェイスを次のように修正する必要があります:

fun{a:t0p}
mergesort{n:nat} (xs: arrayref(a, n), n: int n): arrayref(a, n)

このインターフェイスは、[mergesort] がその2つの引数として配列とその配列のサイズの両方を取ることを意味しています。

配列に対する [myseq_merge] のインターフェイスを次に示します:

fun{a:t0p}
myseq_merge
  {n1,n2:nat}
(
  xs1: arrayref(a, n1), xs2: arrayref(a, n2), n1: int(n1), n2: int(n2)
) : arrayref(a, n1+n2) // end of [myseq_merge]

配列に対する [myseq_merge] の私の実装では、安全でないプログラミングの機能が広範囲に使われています。この方法でコードを書いたのは主に時間を節約することが目的で、配列に対するマージソートのこの実装が実用に向いているわけではありません; 上記で与えられた [mergesort] の仕様的な実装は配列を扱う場合にも適したものである、ということを主張したかったのです。

配列のマージソートの実装全体と追加のテストコードは mergesort_array.dats から入手できます。

改良に基づくプログラミング

上記で示した方法でマージソートのような単純なアルゴリズムを実装するのは、少し杓子定規に思えます。しかし、この改良に基づくプログラミングスタイルは、ある程度複雑なプログラムを書くなら誰にでも魅力的に思えることを私は期待しています。 ATS によってサポートされた抽象型を使うこの作法は、特に改良に基づくプログラミングを最大限に促進する指針で設計されています。私の考えでは、抽象を効果的に使ってプログラミングの複雑さをコントールする能力は、上級プログラマの最も重要な特性です。そして ATS の型システムはこのような能力を習得するのを大いに助けてくれるのです。楽しんでください!

この記事は Hongwei Xi によって書かれ、 Japan ATS User Group によって翻訳されています。