Standard ML雑学

コメントを残す

SML処理系を書いていると必然的にSMLの重箱の隅に詳しくなっていくものである。ここでは筆者が意外だと思ったSMLの仕様を取り上げてみたい。

目次

Standard MLの重箱の隅

ローカルなdatatype

datatypeというのは普通トップレベルとかstructure/functor直下で定義するものだが、実は関数の中でも定義ができる。

fun foo () = let datatype t = MkT in MkT = MkT end;

多相な関数の中で定義されるデータ型の場合、定義の中で関数に紐づいた型変数を参照できる（Successor MLではdatatypeで束縛されたものではない型変数を参照するのは禁止されたようだ）。

fun ''a foo () = let datatype t = MkT of ''a
                 in MkT 123 = MkT 123
                 end;

しかし、ローカルなデータ型の取り扱いを間違えると不健全性に繋がる。次のコードを考えてみよう：

let val r = ref NONE
    fun foo (x : 'a) = let datatype t = MkT of 'a
                           val y = !r
                       in r := SOME (MkT x)
                        ; case y of NONE => NONE | SOME (MkT z) => SOME z
                       end
in foo 123
 ; foo "Hello"
end;

r の型は (〈foo の中の t〉 option) ref と推論される、とする。fooの1回目の呼び出しでは参照 r には SOME (MkT 123) が格納され、2回目の呼び出しではその値が string option として返却される。int の値を string に変換できてしまったということになるので、これはおかしい。

これは、foo の中で定義されたデータ型が外のスコープに漏れ出したのが原因である。

このため、SML ’97ではローカルなデータ型（let式の内部で定義されたデータ型）は外のスコープに脱出できないことになった。この話はThe DefinitionのAppendix G.7で取り上げられている。

Static Semantics for the Core > Inference Rules > Atomic Expressionsの規則4

ローカルなexception

datatypeと同じく、exceptionも関数内で定義できる。さて、関数の中で定義されたexceptionの同一性はどのように判定されるのだろうか？静的に（ソース中の定義位置によって）決まるのか、呼び出しごとにfreshな例外が定義されるのか？

コードで書けば、次のコードは Caught! と Not caught! のどちらを出力するべきか？

fun foo x = let exception Foo
            in if x then
                   raise Foo
               else
                   foo true handle Foo => print "Caught!\n"
            end;
foo false handle _ => print "Not caught!\n";

答えは「呼び出しごとにfreshな例外が定義される」である。上記のコードは Not caught! を出力する。

このことはThe Definitionの6 Dynamic Semantics for the Core > Inference Rules > Exception Bindings の規則130で表されている（と、思う）。

型変数の名前

SMLの型変数はプライム ' から始まる。'a とか 'foo とかそんなやつだ。細かいことを言うと型変数の名前は「識別子にプライムを前置したもの」ではなく「プライムから始まる識別子」なので、正当な識別子ではないものにプライムを前置したもの '0 や、単独のプライム ' も正当な型変数である。

つまり、以下は正当なSMLコードである：

fun f (x : ') = x;
fun g (x : '0) = x;

なお、SML/NJは単独のプライムを拒絶する。

トップレベル宣言と型推論

SMLのトップレベルには通常の（コア言語の）宣言だけでなく、structureやsignature, functorの宣言も書ける。

型推論はセミコロンで区切られたトップレベル宣言の単位で行われる。トップレベル宣言がセミコロンで区切られている時、後の宣言に含まれる式が先の宣言に含まれる式の型推論に影響を及ぼすことはない。

val x = ref NONE
val () = x := SOME 123;

はコンパイルが通るが、

val x = ref NONE;
val () = x := SOME 123;

はコンパイルできるとは限らない。

5 Static Semantics for Modules > Inference Rules > Top-level Declarationsの規則87（tyvars B”=∅あたり）

再帰する方法色々

val recとその構文糖衣（fun, while-do）の他にも再帰する方法はいくつかある。

まず、datatype を使うと再帰的な型を定義できるので、不動点コンビネーターに型をつけることができる：

datatype 'a Rec = MkRec of ('a Rec -> 'a)

val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b
    = fn (f : ('a -> 'b) -> 'a -> 'b) =>
         (fn MkRec x => f (fn (y : 'a) => x (MkRec x) y))
             (MkRec (fn MkRec x => f (fn (y : 'a) => x (MkRec x) y)));

val fact = fix (fn fact => fn n => if n = 0 then 1 else n * fact (n - 1));
print (Int.toString (fact 5) ^ "\n");

次に、参照セルを使った方法もある：

val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b
    = fn f => let val t = ref NONE : (('a -> 'b) option) ref
                  val () = t := SOME (fn x => f (valOf (!t)) x)
              in valOf (!t)
              end;

val fact = fix (fn fact => fn n => if n = 0 then 1 else n * fact (n - 1));
print (Int.toString (fact 5) ^ "\n");

val recを使わない再帰は、「停止性を（保守的に）判定したいコンパイラーが『停止しない可能性がある』と判断しないといけないケース」であり、「コンパイラーが（単なる末尾再帰ではない）真の末尾呼び出し最適化を実装しているかをチェックするテストケース」である。

datatype replicationと型エイリアス

SMLのdatatype replication（datatype foo = datatype bar みたいなやつ）を使うと、他のスコープで定義された型名及び値構築子をそのスコープに持ち込むことができる。

例えば、

datatype order = LESS | EQUAL | GREATER;
structure General = struct
  datatype order = datatype order
end;

と書けば値構築子 LESS に LESS と General.LESS という2つの名前を与えることができる。

型のエイリアスを作るだけなら type 宣言で十分なので、datatype replicationの使用目的は「値構築子を他のスコープに持ち込むこと」と言っていいだろう。

だが、datatype replicationの右辺はdatatypeで定義した型だけではなく、typeで定義した型エイリアスも指定することができる。その場合、値構築子が新たにスコープに持ち込まれることはない。

ちなみに、SML/NJはdatatype replicationの右辺が型エイリアスの場合はエラーを吐く。

SML ’97の変な仕様

SMLは実用的[未定義語]な言語の中では仕様をかなりカッチリ定めている方である。しかし、それでも変な仕様、見方によっては仕様バグと思えるものがあったりする。

value restrictionと多相型

SML ’97ではvalue restrictionと言って val 宣言が多相になるのは右辺がnon-expansiveという分類に当てはまる時に限られる。例えば、 fn x => x という式はnon-expansiveだが ref (fn x => x) はexpansiveである。SMLではvalue restrictionによってこれによって型の不健全性を防いでいる。

しかし、SML ’97の規定では val 宣言の左辺、パターンの部分には特に制約を課していない。例えば、 val SOME f = NONE という宣言では f が多相化されて f : 'a という型がつく。それによって

let val SOME f = NONE
in f ()  (* f の型は unit -> ? として実体化される *)
 ; f "Hello!"  (* f の型は string -> ? として実体化される *)
end

というコードはコンパイルが通る。（もちろん、実行時には Bind 例外が発せられる）

だが、この仕様は多相型のある種のコンパイル方式と相性が悪い。多相の実装方式としては、実行時に型情報（メモリ上のサイズやアラインメント、呼び出し規約などの情報が含まれるかもしれない）を値として受け渡すというものがありうる。この方式（型渡し）では、恒等関数が

val id : 'a -> 'a = fn <type info of 'a> => fn (x : 'a) => x;

とコンパイルされるだろう。そして、先程の val SOME f = NONE は

val f : 'a = fn <type info of 'a> =>
               case NONE ['a] of
                   SOME f => f
                 | _ => raise Bind;

とコンパイルされるだろう。この方式では、 Bind 例外が起こるタイミングが「f が定義された瞬間」ではなく「f に型適用された瞬間」となってしまう。

多相の実装方式としてはMLtonのような「具体的な型について全て展開する方式（テンプレート方式）」もあるが、素朴にやってしまうと「多相な定義が一回も利用されないと定義自体が消去されてしまう」つまり「起きるはずの Bind 例外が起こらなくなってしまう」気がする。なのでそういう処理系ではパターンが非網羅的で束縛結果が一回も利用されない場合はダミーの型について実体化してやる必要がある（MLtonが具体的にどうしているのかは知らない）。

さて、Successor MLでは val 宣言で一般化が起こる要件として「左辺のパターンが網羅的であること」を要件に追加している。これによって先程の let val SOME f = NONE in f () ; f "Hello!" end というコードはコンパイルが通らなくなる。LunarMLでもこれを踏襲する。

ちなみに、LunarMLは動的言語にコンパイルしているので多相の実装方式は型消去に該当する…と言いたいところだが、等価性を持つ型については実行時に比較関数を受け渡すという方式を採用しているのでその辺は型渡しに近い（と言っていいのかな？）。

【追記】初出時はnon-expansiveとexpansiveを取り違えていた。現在は修正済み。

val recでのidentifier statusの上書き

SML ’97では一度値構築子として定義した名前は case で導入する変数名や rec ではない val で導入する変数名として使うことはできない。

datatype t = f;
val f = fn x => x; (* f という変数の定義ではなく f というパターンに対するパターンマッチ（型エラー） *)

しかし、val recはその例外である：

datatype t = f;
val rec f = fn x => x; (* コンパイルが通る！ *)

…が、The DefinitionのDynamic Semanticsではこれは実行時エラーになる（らしい）。

これは仕様バグっぽいのでMLtonやその他のSML処理系は大抵Dynamic Semanticsの解釈を変えて、Bind例外が飛ばないようにしている（HaMLetは律儀にBind例外を飛ばす）。

一方、Successor MLではval recであっても値構築子を上書きできないようにしている。LunarMLでもSuccessor MLの規定に従う。

val recの文法

SML ’97ではval recのrecはand以降に書くことができるし、複数回書くこともできる。

val a = 123
and rec b = fn x => c x
and rec rec rec c = fn x => b x;

しかしこんな書き方を許容してもパーサーが複雑になるだけである。そこで、Successor MLではrecはvalの直後にしか書けないようになった。

val rec b = fn x => b x; (* おなじみ *)

…そこまでは良いのだが、この際に型変数を書ける位置が微妙に変わっている。

val 'a rec id = fn (x : 'a) => x; (* SML '97 互換な書き方 *)
val rec 'a id = fn (x : 'a) => x; (* Successor ML での書き方 *)

まあ普通はval recよりもfunを好んで使うだろうし、型変数を明示する人がどれだけいるのって話で、現実的に影響を受けるコードは少ないだろう。

LunarMLはSML ’97の変なところはSuccessor MLに従って直す・簡素化する方針でいるが、このSML ’97 vs Successor MLの非互換性はちょっと必然性が薄いように思われた。なので、val recの型変数の位置はSML ’97互換な書き方、Successor MLでの書き方の両方を受理するようにしている。（いずれにせよrecは先頭にしか書けないので、SML ’97準拠ではない）

signature内でのtype … and

signatureの中では、他と同じように type 宣言を使って型エイリアスを定義できる。これはderived formとして定義されている。

signature S = sig
  type t = int
   and u = string
end

しかし、SML ’97の規定では and 以後の型の評価に使われる環境がsignature内とその他で微妙に違う。その結果、以下のコードはコンパイルエラーとなる：

type t = int
structure S = struct
  type t = string
   and u = t (* 外の t = int を指す *)
end : sig
  type t = string
   and u = t (* SML '97 では直前の t = string を指す！ *)
end

Successor MLではこの点を修正している（もちろんこれは非互換な変更である）。

SMLに対する拡張

SMLは標準の言語仕様が控えめなので、実用志向な処理系では色々拡張が施されている。C FFIとか。本当は色々書きたかったけど面倒になってしまったのでvector式だけ取り上げる。

vector式（リテラル）とvectorパターン

SML/NJやMLton, Moscow MLはvector式 #[e1,e2,...,en] を実装している。これは vector [e1,e2,...,en] のderived form……と言いたいところだが、SML/NJとMLtonは #[ ] をnon-expansive扱いするので、let多相で多相な型をつけられる。つまり、

val empty = #[];
empty : int vector;
empty : string vector;

はSML/NJとMLtonでコンパイルが通る（Moscow MLではエラーとなる）。なのでこれらのコンパイラー上では #[e1,e2,...,en] は単なるderived formではない。

SML/NJ, MLton, Moscow MLのいずれも、vector式の他にvectorパターンも実装している。

ちなみにMLtonではvector式とvectorパターンはSuccessor MLの一部（allowSuccessorML true で有効になる）扱いされるが、Successor MLのThe Definitionを見てもこれは入ってない。どういうこと？

SMLにおける文字と文字列

SMLの文字と文字列についての話は 自作SML処理系進捗：Hello Lua! に書いてしまった。

自作SML処理系進捗：Hello Lua!

そのうち自作SML処理系にJavaScriptターゲットを実装したいと思っているのだが、標準の string 型をJavaScriptの文字列型（この場合 Char.maxOrd = 65535 とするのが自然）とするか、他の環境との互換性を重視してあくまで8ビット文字列（この場合 Uint8Array を使う）とするか悩んでいる。いずれにせよ WideString はJavaScriptネイティブの文字列を使って提供することになるだろう。

Spread the love

コメントを残す

メールアドレスが公開されることはありません。 ※ が付いている欄は必須項目です