この記事はML Advent Calendar 2014 8日目のために書かれました。

多くの言語においてソートは標準ライブラリで提供されていますが、Standard ML Basis Libraryにはソートを行う関数が存在しません。処理系依存で良ければSML/NJのListMergeSort.sortの様に用意されている場合もある様ですが、ここでは別の方法を考えたいと思います。

方法

処理系依存のライブラリを使いたくないのであれば自前で用意する事になりますが、自分で実装するとなると信頼性を不安に思う事でしょう。

そのような場合にはCoqが便利です。関数の満たすべき性質を証明することでテストでは得られない信頼性が手に入りますし、 Extractionという機能を用いる事でCoqのコードを欲しい言語のコードに変換する事ができます。 SMLのコードへの変換は標準でサポートされていませんが、非公式の改造を施されたCoqを用いればSMLのコードを出力する事ができるようになります。

従って、信頼性の高いコードが得たいのなら

Coqでコードを書く
満たすべき性質を証明する
Extractionによって目的とする言語のコードを出力する

といった手順を辿れば良い事が分かります。幸運な事にマージソートを行う関数がCoqの標準ライブラリで提供されているので、ソートに関しては自分でコードを書いて性質を証明する必要はありません。

結果

Coqのコードとこれによって出力されるSMLのコードを以下に示します。

Require Import Mergesort.
Extraction Language Sml.
Extract Constant app => "(fn x => fn y => x @ y)". 
Extract Inductive option => "option" ["SOME" "NONE"].
Extract Inductive bool => bool ["true" "false"].
Extract Inductive list => "list" ["[]" "(::)"].
Extraction "mergesort.sml" Sort.

(** val app : 'a1 list -> 'a1 list -> 'a1 list **)

val app = (fn x => fn y => x @ y)

signature TotalLeBool' = 
 sig 
  type t 
  
  val leb : t -> t -> bool
 end

functor Sort
  (X:TotalLeBool')  = 
 struct 
  (** val merge : X.t list -> X.t list -> X.t list **)
  
  fun merge l1 l2 =
    let fun merge_aux l3 =
      case l1 of
        [] => l3
      | a1::l1' =>
        (case l3 of
           [] => l1
         | a2::l2' =>
           if X.leb a1 a2 then a1::(merge l1' l3) else a2::(merge_aux l2'))
    in merge_aux l2 end 
  
  (** val merge_list_to_stack :
      X.t list option list -> X.t list -> X.t list option list **)
  
  fun merge_list_to_stack stack l =
    case stack of
      [] => (SOME l)::[]
    | y::stack' =>
      (case y of
         SOME l' => NONE::(merge_list_to_stack stack' (merge l' l))
       | NONE => (SOME l)::stack')
  
  (** val merge_stack : X.t list option list -> X.t list **)
  
  fun merge_stack stack =
    case stack of
      [] => []
    | y::stack' =>
      (case y of
         SOME l => merge l (merge_stack stack')
       | NONE => merge_stack stack')
  
  (** val iter_merge : X.t list option list -> X.t list -> X.t list **)
  
  fun iter_merge stack l =
    case l of
      [] => merge_stack stack
    | a::l' => iter_merge (merge_list_to_stack stack (a::[])) l'
  
  (** val sort : X.t list -> X.t list **)
  
  val sort =
    iter_merge []
  
  (** val flatten_stack : X.t list option list -> X.t list **)
  
  fun flatten_stack stack =
    case stack of
      [] => []
    | o0::stack' =>
      (case o0 of
         SOME l => app l (flatten_stack stack')
       | NONE => flatten_stack stack')
 end

SML/NJの対話環境で実際に試してみるとこんな感じでしょうか。

- use "mergesort.sml";
[opening mergesort.sml]
val app = fn : 'a list -> 'a list -> 'a list
signature TotalLeBool' =
  sig
    type t
    val leb : t -> t -> bool
  end
functor Sort(X: sig
                  type t
                  val leb : t -> t -> bool
                end) :
            sig
              val merge : X.t list -> X.t list -> X.t list
              val merge_list_to_stack : X.t list option list
                                        -> X.t list -> X.t list option list
              val merge_stack : X.t list option list -> X.t list
              val iter_merge : X.t list option list -> X.t list -> X.t list
              val sort : X.t list -> X.t list
              val flatten_stack : 'a list option list -> 'a list
            end
val it = () : unit
- structure Int : TotalLeBool' =
= struct
=   type t = int
=   fun leb a b = a <= b
= end;
structure Int : TotalLeBool'
- structure IntSort = Sort (Int);
structure IntSort :
  sig
    val merge : X.t list -> X.t list -> X.t list
    val merge_list_to_stack : X.t list option list
                              -> X.t list -> X.t list option list
    val merge_stack : X.t list option list -> X.t list
    val iter_merge : X.t list option list -> X.t list -> X.t list
    val sort : X.t list -> X.t list
    val flatten_stack : 'a list option list -> 'a list
  end
- IntSort.sort [1, 1, 4, 5, 1, 4, 8, 10];
val it = [1,1,1,4,4,5,8,10] : Int.t list