ML（プログラミング言語）

ML (Meta Language) は、1970 年代にEdinburgh LCF 定理証明器のために開発されたメタ言語です。これは、 Hindley–Milnerスタイルの多相型推論と、例外や可変変数などのその他の機能を備えた、初期の静的型付け関数型言語です。^{[ 1 ]} ML の LCF における設計は、後の ML ファミリー (特にStandard ML、Caml 、およびそれらの派生)に直接影響を与え、その後の関数型言語の開発にも影響を与えました。^{[ 4 ]}

ML は、ロビン ミルナーが 1973 年にエディンバラ大学に着任した際に、研究助手であるロックウッド モリスとマルコム ニューイの協力を得て開発を開始しました。2 人はともにスタンフォード大学のポスドクで、ミルナーに雇われました。^{[ 5 ]}マイケル ゴードン、クリストファー ワズワース、その他の大学院生が 1975 年までに研究に参加しました。^{[ 4 ]}歴史的に、ML はLCF 定理証明器で証明戦術を開発し、以前のバージョンであるスタンフォード LCF の後継として、スペース利用と証明の拡張性に関する問題を解決しようとして構想されました。ML は、 LCF システムのメタ言語 (そのためこの名前が付けられました) とコマンド ( REPL ) 言語の両方として機能しました。PPLAMBDA は、概念的には一階述語論理と単純型多相ラムダ論理の組み合わせである言語で、定理ステートメントがより直接的に構築される基盤となる言語でした。^{[ 1 ]}

ML が開発されている間、ミルナーは 1978 年に「プログラミングにおける型多相性の理論」という論文を執筆し、多相 (汎用) 型システムのコンテキストでプログラムが適切に型付けされているとはどういうことかという考え方を提示した。彼は、開発した定理のケーススタディ適用として ML を使用し、開発に伴って発生した、まだ解決されていない理論的な課題を指摘した。^{[ 6 ]} ML の最初のバージョンの設計が完成し、その後、1979 年にミルナーがゴードンとワズワースとともに著した書籍「エジンバラ LCF」に文書化された。 ^{[ 5 ] [ 1 ]}

エジンバラ LCF が同名の出版物とともに設立された後、この言語への関心が高まり、設計と機能にわずかな変更を加えた複数の実装が複数の関係者によって進められました。Luca Cardelli はCardelli ML、またはVAX MLを作成し、これは最終的に汎用コンピューティングに適したスタンドアロンの方言に成長し、Unix 下の ML という論文で仕様が定められました。^{[ 7 ] [ 4 ]} InriaのGérard Huet は、 「Project Formel」で Stanford Lisp のソースコードをさまざまな Lisp の方言に移植し始めました。Franz Lispへの移植はLarry Paulsonによってさらに開発され、彼のバージョンは最終的にCambridge LCFと名付けられました。^{[ 8 ]}この LCF のバージョンはその後、 Standard MLの初期バージョンを使用するように更新され、GitHubにアップロードされています。^{[ 9 ]}

当時、ML、LCF、および同時期のプログラミング言語Hopeなどの関連技術に対する注目と興奮が高まっていたことを受け、 Edinburgh LCFのリリースやその他の開発に続いて、1982年11月に「ML、LCF、およびHope」というタイトルの会議が開催されました。この会議では、設計と実装の両方の分裂により重複作業が発生することへの懸念が提起されました。会議ではミルナーは実験精神に寛容な姿勢を示しましたが、その後、バーナード・スフリンとミルナーの間でさらに議論や会議が行われ、スフリンはミルナーにMLの設計を統一するよう促しました。これらのやり取りは、後にミルナーのStandard ML提案の第2草稿で参照されました。^{[ 4 ]}

MLの構文の最も注目すべきインスピレーションは、ISWIMという言語に遡ることができます。ISWIMは「構文糖衣付きラムダ計算」と表現された言語です。 ^{[ 4 ]} MLは、ユーザーがパラメトリック多相性を持つ抽象型を定義でき、コンパイル時にチェックされる強力な静的型システムで設計されました。 ^{[ 1 ]}また、自動型推論機能も備えており、明示的な型注釈を必要とせずに、LispやPOP-2などの当時の動的言語のような使いやすさを実現しました。^{[ 4 ]}

以下の例は、エジンバラ LCFから非常に近い形で派生したもので、ML の構文と機能の概要を示しています。#行頭の文字はユーザー入力を表し、文字のない行は値とその推論された型を示すシステム応答です。このセクションは、ML に含まれる言語機能の包括的なセットとして機能することを意図したものではなく、言語の感覚を与えるためのサブセットであることに注意してください。より厳密な定義については、エジンバラ LCFを参照してください。 ^{[ 1 ]}

式は、式を入力し、その後に;;改行文字を入力することで評価されます。識別子には、it最後に評価された式の結果が格納されます。バインディングはで導入されlet、キーワードで結合するandか、右辺にペア（後の例で説明する積型を持つ）を構築することで、複数のバインディングを同時に作成できます。右辺のペアは左辺に対してパターンマッチングされます。

#2+3;; 5 : int #let x = it;; x = 5 : int #y = 2*5、z = 7 とする;; y = 10 : int z = 7 : int #let x,y,z = y,x,2;; x = 10 : int y = 5 : int z = 2 : int

関数は で定義されますlet。関数の適用は数学演算子よりも優先順位が高いため、 はf 3 + 4を意味します(f 3) + 4。複数のパラメータで定義された関数はカリー化されるため、1 つのパラメータを関数に渡すと、2 番目のパラメータを受け入れる関数が返され、以下同様です。再帰関数は を必要とするletrecため、関数名はその本体内でスコープ内になります。匿名関数の構文はラムダ計算に似ており、\ラムダには 、.引数と式は で区切られます。

#let add xy = x+y;; add = - : (int -> (int -> int)) #3を追加;; - : (int -> int) #it​​ 4;; 7 : int #letrec fact n = if n = 0 then 1 else n * fact(n-1); 事実 = - : (int -> int) #事実4;; 24 : int #(\x.x+1) 3;; 4 : int

リストでは、要素間にセミコロンを使用します。hdと は、tl先頭と末尾を返す組み込み関数です。はcons (先頭に追加).です。は追加です。 のような関数は多態性があり、ML ではこれを表現するために汎用型変数 ( 、、など) を使用します。@hd***

#let m = [1;2;3;4];; m = [1; 2; 3; 4] : (int list) #hd m、tl m;; 1, [2; 3; 4] : (int # (int list)) #0.m @ [5;6];; [0; 1; 2; 3; 4; 5; 6] : (整数リスト) #hd;; - : ((* リスト) -> *) #map (\xx*x) [1;2;3;4];; [1; 4; 9; 16] : (整数リスト)

可変変数は で宣言されletref、 で更新されます:=。loopキーワード は if-then ループ構造に属し、条件が失敗するたびに繰り返されますif。

#事実n = # letref count = n かつ result = 1 # if count = 0 の場合 # その後結果 # ループ count,result := count-1, count*result;; 事実 = - : (int -> int) #事実4;; 24 : int

トークンはMLの文字列型で、`;で区切られます。二重バッククォートはトークンリストを作成します。トークンの一般的な用途はfailwith、明示的なトークンを含む例外を発生させるために使用されるキーワードであるを使用した失敗を識別することであり、?はそれを捕捉するために使用されます。

#`これはトークンです`;; `これはトークンです` : tok #``これはトークンリストです``;; [`this`; `is`; `a`; `token`; `list`] : (tokリスト) #半分のn = # n = 0 の場合は `zero` で失敗します # それ以外の場合は、m = n/2 とする # in if n = 2*m then m else failwith `odd`;; half = - : (int -> int) #半分 4;; 2 : int #ハーフ3;; 評価失敗 奇妙 #半分 3 ? 0;; 0 : int

抽象型は で宣言されabstype、新しい型が作成され、その型を操作する関数が定義されます。内部構造（それが構築された具体的な型）は隠蔽されます。抽象再帰型は で宣言されabsrectype、その型を自身の定義内で使用できるようになります。同様のキーワード があり、これはより基本的な型のエイリアスlettypeに使用されます。以下は、いくつかの基本的な操作を備えた二分木を定義する再帰抽象型です。

#absrectype (*, **) ツリー = * + ** # (*, **) ツリー # (*, **) ツリー # tiptree x = abstree(inl x) を使用 # および comptree (y, t1, t2) = abstree(inr(y, t1, t2)) # そして istip t = isl(reptree t) # そして tipof t = outl(reptree t) ? failwith `tipof` # そして labelof t = fst(outr(reptree t)) ? failwith `labelof` # and sonsof t = snd(outr(reptree t)) ? failwith `sonsof`;; tiptree = - : (* -> (*, **) ツリー) comptree = - : ((** # (*, **) ツリー # (*, **) ツリー) -> (*, **) ツリー) istip = - : ((*, **) tree -> bool) tipof = - : ((*, **) ツリー -> *) labelof = - : ((*, **) tree -> **) sonsof = - : ((*, **) ツリー -> ((*, **) ツリー # (*, **) ツリー))

操作定義（withブロック）内では、型名の前に を付けることで値を型内に囲むことができ、をabs付けることで値を型から切り離すことができます。型定義内の文字と は、それぞれ和型（タグ付き共用体）と積型（タプル）を表し、 の方が優先順位が高くなります。rep+##

ML on LCF は、上記の例で使用されているいくつかのヘルパー関数を提供しています。和型に対しては+、関数inlとがinr和型の左辺または右辺に値を挿入します。outlは左からの挿入から値を抽出し（右からの挿入が指定された場合は失敗します）、はoutr右からの挿入から値を抽出します（左からの挿入が指定された場合は失敗します）。積型の場合#、抽出関数はとでfst、sndペアの最初のコンポーネントと 2 番目のコンポーネントを抽出します。積型は、コンマ中置演算子を使用して構築されます。上記のツリーの例では、comptreeはペアパターンである単一のパラメータを受け取り(y, t1, t2)、ペアを 3 つのコンポーネントに分解します。

• HOL（校正アシスタント）
• Hope（プログラミング言語）
• イザベル（校正アシスタント）
• ヌプル