Successor MLの話

Successor MLとは

Standard MLの仕様は、1997年に出版されたThe Definition of Standard ML (Revised)が最後の版である。しかし、その後も仕様を修正・改良しようという努力が断続的に行われており、Successor MLと呼ばれている。

現行の仕様は以下のGitHubリポジトリーで管理されている：

https://github.com/SMLFamily/Successor-ML

現在のLaTeXではそのままでは処理できないので、https://github.com/SMLFamily/Successor-ML/pull/46の変更を参考にされたい。また、電子的に閲覧したい場合はdefinition/root.texの

%\usepackage{hyperref}

をコメント解除すると良いだろう。ClutTeXを使うと

cd definition && cluttex -epdflatex --bibtex=bibtex root.tex

で処理できる。

ゼロ年代の古いWikiは以下のリンクから辿れる：

https://smlfamily.github.io/successor-ml/

Successor MLの修正点と新機能

細かい修正 (Syntax Fixes / Semantic Fixes)

SML ’97にあった細かい問題が修正されている。

例えば、Appendix E.2では比較演算子 <, >, <=, >= の型が numtxt * numtxt -> numtxt となっているが、これは numtxt * numtxt -> bool の間違いである。

別の例として、ほとんどの処理系が正しく実装していなかった箇所が「修正」される。例えば、

fun foo x true = case x of
                     SOME x' => ()
                   | NONE => ()
  | foo x false = ();

はSML ’97として正当だが、現状これを正しく解釈する処理系は存在しない（らしい）。例えば、標準準拠度が極めて高いMLtonでもこれはUnresolvedBugs扱いされている。

Successor MLでは、「fun宣言の右辺の式は（最後のものを除き）matchで終わってはいけない」という制約を追加することによって現状を追認する。

Monomorphic Non-exhaustive Bindings

SML ’97ではval宣言の右辺だけを見て型の一般化を起こすかどうか判断するので、例えば

val SOME f = SOME (fn x => x);
val SOME g = NONE; (* これは実行時に Bind 例外が出る *)

の f や g には多相な型がついた。しかし、多相なbindingから例外が生じる可能性があるというのは、ある種の処理系（多相の実現に型渡しを採用する処理系）にとって都合が悪い。MLjやSML.NET、それに最近のSML/NJ（110.94以降）はval宣言の左辺が網羅的でない場合には多相な型を付けないようになっている。

Successor MLでは「（右辺が〜〜かつ）左辺が網羅的な場合にのみ型を一般化する」という風に変更している。

Simplified Recursive Value Bindings

SML ’97では次のコードが受理される：

val x = 1 and rec y = fn t => t and rec rec rec z = fn t => t;

つまり、and の後に rec が来ても良いし、rec が複数使われていても良い。

普通はこんなコードを書かないだろうし、構文解析・意味解析が面倒になるだけなので、Successor MLでは val の直後に rec が来なければならないことになった。

val rec y = fn t => t and z = fn t => t;

この際、型変数を書ける位置が変わっているので注意：

val 'a rec f = ... (* SML '97 での書き方（Successor MLでは通らない） *)
val rec 'a f = ... (* Successor ML での書き方（SML '97では通らない） *)

（個人的にはこれは必然性が薄い非互換性だと思ったので、LunarMLでは両方の書き方を受理するようにしている。）

Abstype as Derived Form

abstype というのは抽象型（実装の詳細が隠蔽された型）を作るための機構で、Standard MLにモジュールシステムが入る前の遺物らしい。単に古いというだけでなく、abstypeはequalityに関して厄介な性質を持っている。次のコードを考える：

abstype t = T with
fun eqT (x, y) = x = y
end

abstypeの中では、型 t はequalityを許容する（= で比較できる）が、外では t はequalityを許容しない。ここで、 eqT は t に関する比較関数のつもりで定義したのに、多相型 ''a * ''a -> bool が推論されてしまうとabstypeの外では eqT を t に使えなくなってしまう。

Successor MLはこのequalityに関する挙動を変えて、abstypeは定義される型のequalityを隠さないようになった。この変更により、abstypeはderived form（構文糖衣）として定義できるようになる。

MLtonではこの件はSuccessor ML準拠の挙動となっており、SML ’97的にはUnresolvedBugs扱いされている。

Fixed Manifest Type Specifications

Standard MLでは and で繋がれた宣言は、型や変数の環境的には「同時」に行われる。例えば、

val x = 42;
val x = 37 and y = x + 1;

というプログラムでは2行目の x と y の右辺は x のシャドーイングが起こる前の環境で評価され、 y には43（38ではなく）が束縛される。

型についても同様で、

type t = int;
type t = string
 and u = t * t;

という宣言では、u には string * string ではなく int * int が束縛される。

ところが、signature中の型宣言は例外で、

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

という宣言では u は string * string になってしまう。

Successor MLではsignature中での型宣言を修正し、先の例では u に int * int が束縛されるようにする。

Abolish Sequenced Type Realisations

signatureが含む型変数を実体化するときは where type 節を使う：

signature S = sig
  type t
  val x : t
end;
structure T = struct ... end : S where type t = int;

where type で型を複数実体化するためにSML ’97では and type という構文が用意されていた：

signature S = sig
  type t
  type u
  ...
end;
structure T = struct ... end : S where type t = int
                                   and type u = string

が、パーサーが複雑になるのと、単に where type を複数書けば済むということで、Successor MLでは and type は廃止された。

Line Comments

Standard MLではネスト可能なコメント (* ... *) が使えるが、行コメントはなかった。

Successor MLでは (*) から始まる行コメントが導入される。

行コメントは (* … *) の内側でも効果を発揮する。例えば、

(*
fun f x = ... (*) すごい関数 *)
*)

の2行目の最後の *) の効果は行コメントで打ち消され、全体として一つのコメントとなる。

Extended Literal Syntax

リテラルについて、何点か拡張される。

まず、数値リテラルの数字をアンダースコアで区切れるようになる。

次に、整数リテラルを接頭辞 0b または 0wb により二進表記できるようになる。

最後に、（HaMLet Sには実装されていないのでこの括りで紹介するのが適切かは分からないが）文字列リテラル中に \Uxxxxxxxx （x は十六進）でコード値が大きい文字を書けるようになる。まあSMLで使われるのはバイト文字列（Char.maxOrd = 255）が中心なのでぶっちゃけ \U の使い所はないと思う。

Record Punning

これまでのStandard MLではレコードパターンの { field = field } を省略して { field } と書けた。

Successor MLではレコードの値の方でも同じような省略ができるようになる。

Record Extension

フィールドが多いレコードからフィールドの一部を追加または削除したい場合、従来は全てのフィールドを改めて列挙する必要があった。

Successor MLでは、フィールドの削除はレコード拡張パターンで

fun f someRecord = case someRecord of
                     { field1 = _, ... = rest } => rest

と書ける。ここで rest は someRecord からフィールド field1 を取り除いたレコードになる。

フィールドの追加は

val newRecord = { field2 = "Yes!", ... = someRecord };

と書ける。

型レベルでもフィールドの追加ができる。

type t = { foo : int }
type u = { bar : string, ... : t } (* u は { bar : string, foo : int } と等価 *)

Record Update

フィールドが多いレコードの一部のフィールドだけを更新したい場合がある。従来のStandard MLでは全てのフィールドを列挙し直す必要があったが、Successor MLではrecord updateが使える。

val newRecord = { someRecord where field1 = "new value" }

これはrecord extensionのderived formとして定義されている。

更新後のフィールドの型は異なっていても良い。例えば、

fun f (r as { x, y }) = { r where x = 1 };

という関数 f の型は { x : 'b, y : 'a } -> { x : int, y : 'a } となる。

これはSML#が独自に実装している「フィールドアップデート式」 https://smlsharp.github.io/ja/documents/4.0.0/Ch19.S11.html との違いである。SML#では

# fun f (r as { x, y }) = r # { x = 1 };
val f = fn : ['a. {x: int, y: 'a} -> {x: int, y: 'a}]

となる（更新前のフィールドも同じ型を持たなければならない）。SML#はSuccessor MLには与せず独自路線を行く印象である。

Conjunctive Patterns

SML ’97では 変数名 as パターン という感じでパターンマッチする構造の一部を変数で束縛できたが、Successor MLでは as の左側にもパターンを書けるようになる。

これにより、 パターン as 変数名 という書き方もできるようになる。このほか、後述するnested matchとの組み合わせも有用そうだ。

Disjunctive Patterns

いくつかの異なるパターンを同じ分岐で処理したい場合がある。例えば、

fun f #"a" = 処理1
  | f #"A" = 処理1
  | f x = 処理2

という関数定義があったときに処理1を2回書きたくない。

Successor MLでは

fun f (#"a" | #"A") = 処理1
  | f x = 処理2

と、複数のパターンを | で繋いで書けるようになる。

Nested Matches

パターン中でさらなるパターンマッチができるようになる。文法は

パターン1 with パターン2 = 式

である。例えば、次のコードが書けるようになる：

fun f (x with SOME y = SomeTable.lookup x) = y
  | f _ = 42

Pattern Guards

パターン中に条件が書けるようになる。文法は

パターン if 式

である。例は

fun f (x if Char.isAlpha x) = "alphabet"
  | f _ = "not alphabet"

これはnested matchのderived formとして定義される。例えば、例のコードは

fun f (x with true = Char.isAlpha x) = "alphabet"
  | f _ = "not alphabet"

と書き直せる。

Optional Bars and Semicolons

SMLではパターンやデータ型の構築子は縦棒 | で区切られる。従来は最初の要素の前には縦棒を置くことができなかったが、Successor MLでは最初の要素の前にも縦棒を置けるようになる。

例：

case x of
  | SOME y => y
  | NONE => "default"

Optional else Branch

「条件がtrueの時だけある処理を実行したい」という場合に

if cond then
    someAction ()
else
    ()

という、else節に () だけを書くパターンは頻出である。Successor MLではこの場合に

if cond then
    someAction ()

と書くことができるようになる。

文法上の曖昧さ、つまりdangling else問題は「最も内側のifと組み合わせる」という形で解決される。

パーサーの複雑さが増えるので個人的には好きではない。

Do Declarations

宣言の中でアクションを実行する際に

val () = someAction ()

と書くパターンは頻出である。Successor MLではこれを

do someAction ()

と書けるようになる。

Withtype in Signatures

まずはwithtypeについて。SMLではtypeで定義する型は自身を参照できず、datatypeで定義する型は自身を参照できる。レコード型の中で自身と同型な型を参照したい場合は

datatype Env' = MkEnv of { valueMap : v map, structureMap : Env' map }
type Env = { valueMap : v map, structureMap : Env' map }
(*
本当は
type Env = { valueMap : v map, structureMap : Env map }
と書きたいけどtypeでは自身を参照できないので仕方なく……
*)

という風に書くしかないのだが、SMLではこのパターンに対するderived formとしてwithtypeというのが用意されている。withtypeを使うと先の宣言は

datatype Env' = MkEnv of Env  (* 直後の型エイリアスを参照できる *)
withtype Env = { valueMap : v map, structureMap : Env' map }

と書ける。

SML ’97ではwithtypeはsignatureの中には書けなかったが、Successor MLではsignatureの中にもwithtypeを書けるようになる。

処理系での実装状況

いくら仕様があっても処理系に実装されなければ意味がない。ここでは、Successor MLまたはその一部を実装した処理系を紹介する。

HaMLet S

HaMLetという、「Standard MLのリファレンス実装を目指す」処理系がある。

HaMLet SはそのSuccessor ML版、というかSuccessor MLのための実験場で、Successor MLのほとんどを実装しているほか、独自の拡張を色々実装している。

HaMLet SはHaMLetと同じリポジトリーのsuccブランチで管理されている。

Successor MLのうち、 \Uxxxxxxxx には対応してなさそうである。

HaMLet SのマニュアルはSuccessor MLの資料として有用である。HaMLet Sのdoc/Manual.texの \usepackage[dvips=true,...]{hyperref} の dvips=true を削った上で

cd doc && cluttex -exelatex Manual.tex

とするとPDF化できる（PSTricksを使っているため、pdfLaTeXで処理するのは面倒である）。

SML/NJ

SML/NJは色々拡張機能を提供しており、そのうちSuccessor MLと被る物もある（withtype in signaturesとor patterns）。また、最近のバージョンではSuccessor MLの一部（軽量な機能）を取り込んでいるほか、標準ライブラリーに対する拡張も実装している。

昔から：withtype in signatures, or patterns（disjunctive patternsと同等だが、カッコが必須）
- https://www.smlnj.org/doc/features.html
110.79（2015年10月4日）: https://www.smlnj.org/dist/working/110.79/110.79-README.html
- extended literals: アンダースコア、二進リテラル
- 一行コメント (*)
- 標準ライブラリーの拡張：ListPairの修正、Either, 列に対する操作、Fn, Ref
- 有効化の方法は Control.succML 変数または -Cparser.succ-ml=true オプションまたはCMファイル中での指定
110.81（2017年5月1日）: https://www.smlnj.org/dist/working/110.81/110.81-README.html
- record pun
- do宣言
- 有効化の方法は Control.succML の代わりに Control.setSuccML : bool -> unit になった。
110.94（2019年10月31日）: https://www.smlnj.org/dist/working/110.94/110.94-README.html
- val宣言で定義される変数が多相化される条件に、「パターンが網羅的であること」が追加された。これはSuccessor MLでの変更点と一致する。
110.98（2020年7月17日）: https://www.smlnj.org/dist/working/110.98/110.98-README.html
- Universalモジュール

機能別チェックリスト：

☑︎Monomorphic non-exhaustive bindings
☐Simplified recursive value bindings
☐Abstype as derived form
☐Fixed manifest type specifications
☐Abolish sequenced type realizations
☑︎Line comments
Extended literal syntax: ☑︎Numeric / Text
☑︎Record punning
☐Record extension
☐Record update
☐Conjunctive patterns
– Disjunctive patterns
☐Nested matches
☐Pattern guards
Optional bars and semicolons: bars
☐Optional else branch
☑︎Do declaration
☑︎Withtype in signatures

MLton

MLtonもSuccessor MLの機能の一部を実装している。詳しくは以下のページを参照：

チェックリスト：

☐Monomorphic non-exhaustive bindings
☐Simplified recursive value bindings
☑︎Abstype as derived form
☐Fixed manifest type specifications
☐Abolish sequenced type realizations
☑︎Line comments (allowLineComments)
☑︎Extended literal syntax: Numeric / Text (allowExtendedConsts / allowExtendedNumConsts / allowExtendedTextConsts)
☑︎Record punning (allowRecordPunExps)
☐Record extension
☐Record update
☐Conjunctive patterns
☑︎Disjunctive patterns (allowOrPats)
☐Nested matches
☐Pattern guards
☑︎Optional bars and semicolons (allowOptBar / allowOptSemicolon)
☐Optional else branch
☑︎Do declaration (allowDoDecls)
☑︎Withtype in signatures (allowSigWithtype)

LunarML

LunarMLは筆者が作っている新しいStandard ML処理系であり、なるべくSuccessor ML準拠にしたいと思っている。

現在の機能別チェックリスト：

☑︎Monomorphic non-exhaustive bindings
☑︎Simplified recursive value bindings
☑︎Abstype as derived form
☑︎Fixed manifest type specifications
☐Abolish sequenced type realizations
☐Line comments
☐Extended literal syntax
- ☑︎Underscores
- ☑︎Binary constant
- ☐\Uxxxxxxxx
☐Record punning
☑︎Record extension
☑︎Record update
☐Conjunctive patterns
☐Disjunctive patterns
☐Nested matches
☐Pattern guards
☐Optional bars and semicolons
☐Optional else branch
☐Do declarations
☑︎Withtype in signatures

Record extension / updateを実装したのは我ながら偉いと思う。あとはパターンマッチに関するものを実装すれば、Successor MLは制覇したと言って過言ではなくなるのだが……。

ただ、optional else branchはパーサーを複雑にするので、採用しない可能性もある（Successor MLにはコンパイラーを単純にする趣旨の変更がちょいちょいあるのに、optional else branchはそれに反しているように見える）。

Spread the love

雑記帳

人生やっていき