LCF MLについて
この記事はML Advent Calendar 2014 24日目のために書かれました。
Standard MLをはじめとするML系言語の始祖として、よくLCF MLの名前が挙げられます。 ここでは、LCF MLの言語機能について解説しつつ後の言語に与えた影響について思いを馳せたいと思います。
編集履歴
2014/12/24 2:46 抽象データ型のサンプルコードで直積と直和を間違えている部分があったので修正
LCF MLとは
名前の表す通り、LCFという定理証明系のメタ言語として開発された言語です。
LCFの実装はエディンバラ大学でDEC 10上のLispによって行われたそうで、 開発された時代を感じる事ができます。 その成立は1972年ですから、C言語と同時期の言語ですね。
C言語と同時期の言語というとどこか古臭そうな印象を受けますが、 LCF MLは式を基調とした関数型言語であるものの破壊的代入などといった副作用を伴った式を書ける、 例外のようなエラー処理機能を有している、型推論を行う静的型付き言語であるなど、 現代のMLの原型を見る事ができます。
変数束縛
e'を評価する間、eを評価して得られる値を変数xに束縛したい場合、let x = e in e'と書きます。 同様に、関数の定義を行いたい場合はlet f(x,y,...)=e、再帰関数の定義を行いたい場合はletrec f(x,y,...)=e（あまり積極的に用いられていないものの、let f x y ... = eと書く事でカリー化された関数も書けるらしい[1]）、 書き換え可能な変数xをeを評価した結果を初期値として定義する場合はletref x=eと書きます。 この点はStandard MLよりOCamlに近い構文ではないでしょうか。
相互再帰的な関数が書きたければlet x = e1 where y = e2 ...、letrec x = e1 whererec y = e2 ...と書きます。
対話環境で複数の定義を行う場合、お察しの通り;;で区切るようです。（"In interactive programming ... one evaluates a mixed sequence of declarations and expressions, separated by ";;"."[1]）
エラー処理
エラー処理に関しては例外をサポートする現代のML系言語とは趣が違い、 さながらfailureという一種類の例外のみをサポートしているような印象を受けます。
式e ? e'はeの評価した結果failureを生成しなければeを評価した結果に、 failureを生成すればe'を評価した結果に評価されます。 OCamlで言う所のtryやSMLで言う所のhandleに近いのではないでしょうか。
式failを評価するとfailureを生成します。OCamlやSMLで言う所のraiseといった感じでしょうか。
型システム
多相関数や多相データ型をサポートする静的型付き言語であり、 型推論が行われるため変数を宣言する際には型注釈の必要はありません。
明示的に型を書きたい場合、letrec f (x : t1) : t2 = ...の様に書く事ができます。 直積型はα×β、多相データ型は型パラメータを前に置いてα listの様に書きます。 この辺りはOCamlやSMLといった現代のML系言語に近いですね。
少し趣が異なる所と言えばα+βが直和、.が()のみを要素に持つ型である事でしょうか。
抽象データ型の定義
自分で抽象データ型を定義したい場合、abstype
with以降にはその抽象データ型を操作する関数の定義を書きます。 ここで、with以降に書いた抽象データ型を操作した関数ではabsidという名前の定義にあたる型の値を受け取って等価な抽象データ型の値を返す関数と、 repidという名前の抽象データ型の値を受け取って等価な定義にあたる型の値を返す関数を使う事ができます。 早い話がキャストのようなものです。 型システムとの兼ね合いでこういうキモい関数が必要になったのではないかと。
型の定義は複数同時に行う事ができ、複数同時に行う場合はabstype
再帰データ型を定義する場合はabstypeの代わりにabsrectypeと書きます。
多分何を言っているのか分からないと思うのでリストを定義する場合のコードを示します。[1]
absrectype α list = . + (α × α list) with nil = abslist(inl()) and $.(x,l) = abslist(inr(x, l)) and null(l) = isl(replist(l)) and hd(l) = fst(outr(replist(l))) and tl(l) = snd(outr(replist(l)))
ここで、
abslist : (. + (α × α list))→α list replist : α list→(. + (α × α list)) inl : α→α+β inr : β→α+β isl : α+β→bool outr : α+β→β fst : α×β→α snd : α×β→β
です。型から察せない関数について補足すると、islは引数で与えられたα+β型の値がα型の値から作られたものかどうかを返す関数です。 outrは引数で与えられたα+β型の値がβ型の値から作られたものでない場合はfailureを生成します。
この辺りは現代のML系言語とは大分趣が異なりますね。 ML系言語も進化しているという事でしょうか。
その他
最後に
C言語と同時期に既にこのような言語が存在していたのは驚きです。 最近になって関数型言語が騒がれていますが、今回参考にした1978年の文章[1]には既に "functional programming language"という言葉が登場している事からも、その歴史は決して短いものではないと感じられます。
この記事を読んでLCF MLのより詳細な仕様が気になる場合は、参考資料[1]で紹介されていたGordon, M., Milner, R. & Wadsworth, C. Edinburgh LCF, Department of Computer Science International Report CSR-11-77, University of Edinburgh, 1977.をお勧めします。
