Loading article…
Standard ML ( SML ) は、コンパイル時の型チェックと型推論を備えた、汎用性の高い高水準のモジュール型関数型プログラミング言語です。コンパイラの作成、プログラミング言語の研究、定理証明器の開発などに広く利用されています。
Standard ML は、計算可能な関数の論理(LCF) 定理証明プロジェクトで使用される言語であるMLの現代版です。広く使用されている言語の中で際立っているのは、形式仕様を持っていることです。形式仕様は、1990 年に最初に公開され、1997 年に 2 回目で最終版が公開された「Standard ML の定義」に、型規則と操作的意味論として記載されています。[ 5 ] [ 6 ]
Standard ML は、一部に非純粋な機能を持つ関数型プログラミング言語です。Standard ML で記述されたプログラムは、文やコマンドとは対照的に式で構成されますが、ユニット型の式の中には副作用のみを評価するものもあります。
すべての関数型言語と同様に、Standard ML の重要な特徴は、抽象化に使用される関数です。階乗関数は次のように表現できます。
fun factorial n = if n = 0 then 1 else n * factorial ( n - 1 )SMLコンパイラは、ユーザーが型注釈を指定しなくても静的型を推論する必要があります。つまり、 は整数式でのみ使用されるため、それ自体が整数型であること、そしてすべての終端式が整数式であることを推論しなければなりません。valfactorial:int->intn
同じ機能は、if - then - else条件文を特定の値に対して評価した階乗関数のテンプレートに置き換えた節関数定義によって表現することもできます。
fun factorial 0 = 1 | factorial n = n * factorial ( n - 1 )または反復的に：
fun factorial n = let val i = ref n and acc = ref 1 in while !i > 0 do ( acc := !acc * !i ; i := !i - 1 ); !acc endまたはラムダ関数として：
val rec factorial = fn 0 => 1 | n => n * factorial ( n - 1 )ここで、キーワードはval識別子と値の結合を導入し、匿名関数fnを導入し、定義が自己参照的になることを可能にします。rec
ここに示されているように、不変条件を保持する末尾再帰的なタイトループを、1つ以上のアキュムレータパラメータとともに、不変条件を含まない外側の関数内にカプセル化することは、Standard ML でよく用いられるイディオムです。
ローカル関数を使用することで、より効率的な末尾再帰スタイルで書き直すことができます。
local fun loop ( 0 , acc ) = acc | loop ( m , acc ) = loop ( m - 1 , m * acc ) in fun factorial n = loop ( n , 1 ) end型シノニムはキーワードで定義されます。以下は平面type上の点を表す型シノニム、および2点間の距離を計算する関数、ヘロンの公式に従って指定された頂点を持つ三角形の面積を計算する関数です。（これらの定義は以降の例で使用されます。）
type loc = real * realfun square ( x : real ) = x * xfun dist ( x , y ) ( x' , y' ) = Math.sqrt ( square ( x' - x ) + square ( y ' - y ) )fun heron ( a , b , c ) = let val x = dist a b val y = dist b c val z = dist a c val s = ( x + y + z ) / 2.0 in Math . sqrt ( s * ( s - x ) * ( s - y ) * ( s - z )) endStandard MLは、代数的データ型（ADT）を強力にサポートしています。データ型は、タプルの非連結和（または「積の和」）と考えることができます。パターンマッチング、そしてほとんどのStandard ML実装におけるパターン網羅性チェックとパターン冗長性チェックのおかげで、データ型は簡単に定義でき、簡単に使用できます。
オブジェクト指向プログラミング言語では、非連結和集合はクラス階層として表現できます。しかし、クラス階層とは対照的に、ADTは閉じています。したがって、ADTの拡張性とクラス階層の拡張性は直交します。クラス階層は同じインターフェースを実装する新しいサブクラスで拡張できますが、ADTの関数は固定されたコンストラクタセットに対してのみ拡張できます。式の問題を参照してください。
データ型は、次のようにキーワードを使用して定義されますdatatype。
データ型shape = loc * real (* 中心と半径 *)の円| loc * real (* 左上隅と辺の長さ、軸に平行 *)の正方形| loc * loc * loc (* 角 *)の三角形型シノニムは再帰的であってはならないことに注意してください。再帰的なコンストラクタを定義するにはデータ型が必要です。（この例ではこの点は問題になりません。）
パターンは定義された順序で照合されます。C言語のプログラマは、タグ付き共用体を使用し、タグ値に基づいてディスパッチすることで、MLがデータ型とパターンマッチングで行っていることを実現できます。ただし、適切なチェックで装飾されたCプログラムは、ある意味では対応するMLプログラムと同じくらい堅牢ですが、それらのチェックは必然的に動的になります。MLの静的チェックは、コンパイル時にプログラムの正しさについて強力な保証を提供します。
関数の引数は、以下のようにパターンとして定義できます。
面積(円(_, r )) = Math . pi * square r |面積(正方形(_, s )) = square s |面積(三角形p ) = heron p ( * 上記参照 *)関数定義におけるいわゆる「節形式」、すなわち引数をパターンとして定義する形式は、単にケース表現の構文糖衣に過ぎない。
楽しい領域の形状=円の形状( _ , r ) => Math.pi * square r |正方形(_, s ) => square s |三角形p = > heron pパターン網羅性チェックにより、データ型の各コンストラクタが少なくとも1つのパターンに一致することが保証されます。
以下のパターンは網羅的なものではありません。
fun center ( Circle ( c , _)) = c | center ( Square (( x , y ), s )) = ( x + s / 2.0 , y + s / 2.0 )Triangle関数内にはケースのパターンがありませんcenter。コンパイラはケース式が網羅的ではないという警告を発し、Triangle実行時にこの関数に が渡された場合は例外が発生します。exceptionMatch
以下の（意味のない）関数の2番目の節のパターンは冗長です。
fun f ( Circle (( x , y ), r )) = x + y | f ( Circle _) = 1.0 | f _ = 0.02番目の節のパターンに一致する値はすべて、1番目の節のパターンにも一致するため、2番目の節には到達できません。したがって、この定義全体に冗長性があり、コンパイル時に警告が発生します。
以下の関数定義は網羅的であり、冗長ではありません。
val hasCorners = fn ( Circle _) => false | _ => true制御が最初のパターン（Circle）を通過すると、形状はまたSquareはのいずれかであることがわかりますTriangle。どちらの場合も、形状には角があることがわかっているので、true実際の形状を判別せずに処理を終了できます。
関数は、引数として関数を受け取ることができます。
楽しいマップf ( x , y ) = ( f x , f y )関数は戻り値として関数を生成することができます。
関数定数k = ( fn _ => k )関数は、関数を消費することも、関数を生成することもできます。
fun compose ( f , g ) = ( fn x => f ( g x ))List.map基本ライブラリの関数は、Standard MLで最もよく使用される高階関数の1つです。
fun map _ [] = [] | map f ( x :: xs ) = f x :: map f xs末尾再帰によるより効率的な実装List.foldl：
fun map f = List.rev o List.foldl ( fn ( x , acc ) = > f x :: acc ) [ ]例外はキーワードで発生しraise、パターンマッチングhandle構造で処理されます。例外システムは非ローカル終了を実装できます。この最適化手法は、次のような関数に適しています。
local exception Zero ; val p = fn ( 0 , _) => raise Zero | ( a , b ) => a * b in fun prod xs = List . foldl p 1 xs handle Zero => 0 end例外が発生すると、制御は関数から完全に抜けます。別の方法を考えてみましょう。値 0 が返され、それがリスト内の次の整数と乗算され、結果の値 (必然的に 0) が返され、以下同様です。例外が発生すると、制御はフレームのチェーン全体をスキップし、関連する計算を回避できます。アンダースコア ( ) がワイルドカードパターンとして使用されていることに注意してください。exceptionZeroList.foldl_
末尾呼び出しでも同様の最適化が得られます。
local fun p a ( 0 :: _) = 0 | p a ( x :: xs ) = p ( a * x ) xs | p a [] = a in val prod = p 1 endStandard MLの高度なモジュールシステムでは、プログラムを論理的に関連付けられた型と値の定義からなる階層構造に分解できます。モジュールは名前空間の制御だけでなく、抽象データ型の定義を可能にするという意味での抽象化も提供します。モジュールシステムは、シグネチャ、構造体、ファンクタという3つの主要な構文構造で構成されています。
シグネチャはインターフェースであり、通常は構造体の型として考えられます。シグネチャは、構造体によって提供されるすべてのエンティティの名前、各型コンポーネントのアリティ、各値コンポーネントの型、および各サブ構造体のシグネチャを指定します。型コンポーネントの定義は省略可能です。定義が隠蔽されている型コンポーネントは抽象型です。
例えば、キューのシグネチャは次のようになります。
signature QUEUE = sig type 'a queue exception QueueError ; val empty : 'a queue val isEmpty : 'a queue -> bool val singleton : 'a -> 'a queue val fromList : 'a list -> 'a queue val insert : 'a * 'a queue -> 'a queue val peek : 'a queue -> 'a val remove : 'a queue -> 'a * 'a queue endこのシグネチャは、多相型、およびキューに対する基本操作を定義する値を提供するモジュールを記述しています。'aqueueexceptionQueueError
構造体はモジュールの一種であり、型、例外、値、構造体（サブ構造体と呼ばれる）の集合が論理的な単位としてパッケージ化されて構成されます。
キュー構造は以下のように実装できます。
構造体TwoListQueue :> QUEUE = struct type 'a queue = 'a list * 'a list例外QueueError ;val empty = ([], [])fun isEmpty ([], []) = true | isEmpty _ = falsefun singleton a = ([], [ a ])fun fromList a = ([], a )fun insert ( a , ([], [])) = singleton a | insert ( a , ( ins , outs )) = ( a :: ins , outs )fun peek (_, []) = raise QueueError | peek ( ins , outs ) = List . hd outsfun remove (_, []) = raise QueueError | remove ( ins , [ a ]) = ( a , ([], List . rev ins )) | remove ( ins , a :: outs ) = ( a , ( ins , outs )) endこの定義は、がを実装することを宣言しています。さらに、で示される不透明な属性は、シグネチャで定義されていない型（つまり）は抽象型であるべきであることを示しており、リストのペアとしてのキューの定義はモジュールの外部からは見えないことを意味します。構造体は、シグネチャ内のすべての定義を実装しています。structureTwoListQueuesignatureQUEUE:>type'aqueue
構造体内の型と値には、「ドット表記」を使用してアクセスできます。
val q : string TwoListQueue . queue = TwoListQueue . empty val q' = TwoListQueue . insert ( Real . toString Math . pi , q )ファンクタとは、構造体から構造体への関数です。つまり、ファンクタは、通常は特定のシグネチャを持つ構造体である1つ以上の引数を受け取り、結果として構造体を生成します。ファンクタは、汎用的なデータ構造やアルゴリズムを実装するために使用されます。
木構造の幅優先探索によく用いられるアルゴリズムの一つに、キューを利用するものがあります。[ 7 ]以下は、抽象的なキュー構造に基づいてパラメータ化された、そのアルゴリズムのバージョンです。
(* Okasaki、ICFP、2000 に倣って *) functor BFS ( Q : QUEUE ) = struct datatype 'a tree = E | T of 'a * 'a tree * 'a treelocal fun bfsQ q = if Q . isEmpty q then [] else search ( Q . remove q ) and search ( E , q ) = bfsQ q | search ( T ( x , l , r ), q ) = x :: bfsQ ( insert ( insert q l ) r ) and insert q a = Q . insert ( a , q ) in fun bfs t = bfsQ ( Q . singleton t ) end end構造QueueBFS = BFS ( TwoListQueue )内部では、キューの表現は可視化されません。より具体的には、実際に使用されている表現が2つのリストからなるキューである場合、最初のリストを選択する方法はありません。このデータ抽象化メカニズムにより、幅優先探索はキューの実装に完全に依存しなくなります。これは一般的に望ましいことであり、この場合、キュー構造は、その正しさが依存する論理的不変条件を、堅牢な抽象化の壁の背後で安全に維持できます。functorBFS
SML コードの断片は、対話型のトップレベルに入力することで最も簡単に学習できます。
以下は「ハローワールド！」プログラムです。
挿入ソート（昇順）は、以下のように簡潔に表現できます。intlist
fun insert ( x , []) = [ x ] | insert ( x , h :: t ) = sort x ( h , t ) and sort x ( h , t ) = if x < h then [ x , h ] @ t else h :: insert ( x , t ) val insertionsort = List . foldl insert []ここでは、古典的なマージソートアルゴリズムが、split、merge、mergesort の 3 つの関数で実装されています。また、リストを表す構文とを除いて、型がないことにも注意してください。このコードは、一貫した順序付け関数が定義されている限り、任意の型のリストをソートします。Hindley –Milner 型推論を使用すると、関数のような複雑な型であっても、すべての変数の型を推論できます。op::[]cmpcmp
スプリット
funsplitは、とを交互に切り替えるステートフルクロージャで実装され、入力は無視されます。truefalse
fun alternator {} = let val state = ref true in fn a => !state before state := not ( !state ) end(* リストをほぼ半分に分割します。半分の長さは同じか、または最初の半分がもう一方より要素が1つ多くなります。* 実行時間はO(n)です。ここでn = |xs|です。*) fun split xs = List . partition ( alternator {}) xsマージ
Merge は効率化のためにローカル関数ループを使用します。内部は、両方のリストが空でない場合 ( ) と、一方のリストが空の場合 ( )loopのケースで定義されます。x::xs[]
この関数は、2 つのソート済みリストを 1 つのソート済みリストにマージします。アキュムレータが逆順に構築され、その後反転されて返される点に注目してください。これは、がリンク リストとして表現されるaccため、一般的な手法です。この手法はより多くのクロック時間を必要としますが、漸近的な結果は悪化しません。'alist
(* 順序付きリスト 2 つを順序付き cmp を使用してマージします。* 前提条件: 各リストは、cmp ごとに既に順序付けされている必要があります。* 実行時間は O(n) です。ここで、n = |xs| + |ys| です。* ) fun merge cmp ( xs , [ ] ) = xs | merge cmp ( xs , y :: ys ) = let fun loop ( a , acc ) ( xs , []) = List . revAppend ( a :: acc , xs ) | loop ( a , acc ) ( xs , y :: ys ) = if cmp ( a , y ) then loop ( y , a :: acc ) ( ys , xs ) else loop ( a , y :: acc ) ( xs , ys ) in loop ( y , [] ) ( ys , xs ) endマージソート
主な機能：
fun ap f ( x , y ) = ( f x , f y )(* 指定された順序付け操作 cmp に従ってリストをソートします。* 実行時間は O(n log n) です。ここで n = |xs| です。*) fun mergesort cmp [] = [] | mergesort cmp [ x ] = [ x ] | mergesort cmp xs = ( merge cmp o ap ( mergesort cmp ) o split ) xsクイックソートは次のように表現できます。は順序演算子 を消費するクロージャです。funpartop<<
中置<<fun quicksort ( op << ) = let fun part p = List . partition ( fn x => x << p ) fun sort [] = [] | sort ( p :: xs ) = join p ( part p xs ) and join p ( l , r ) = sort l @ p :: sort r in sort end小規模な式言語は、比較的容易に定義および処理できることに注目してください。
例外TyErr ;データ型ty = IntTy | BoolTyfun unify ( IntTy , IntTy ) = IntTy | unify ( BoolTy , BoolTy ) = BoolTy | unify (_, _) = raise TyErrデータ型exp = True | False | intのint 型| expのNot 型| exp * expのAdd 型| exp * exp * expのIf型fun infer True = BoolTy | infer False = BoolTy | infer ( Int _) = IntTy | infer ( Note e ) = ( assert e BoolTy ; BoolTy ) | infer ( Add ( a , b )) = ( assert a IntTy ; assert b IntTy ; IntTy ) | infer ( If ( e , t , f )) = ( assert e BoolTy ; unify ( infer t , infer f )) and assert e t = unify ( infer e , t )fun eval True = True | eval False = False | eval ( Int n ) = Int n | eval ( Note e ) = if eval e = True then False else True | eval ( Add ( a , b )) = ( case ( eval a , eval b ) of ( Int x , Int y ) => Int ( x + y )) | eval ( If ( e , t , f )) = eval ( if eval e = True then t else f )fun run e = ( infer e ; SOME ( eval e )) handle TyErr => NONE型付けが正しい式と型付けが間違っている式での使用例：
val SOME ( Int 3 ) = run ( Add ( Int 1 , Int 2 )) (* 型付けが正しい *) val NONE = run ( If ( Not ( Int 1 ), True , False )) (* 型付けが間違っている *)このIntInfモジュールは任意精度整数演算機能を提供します。さらに、プログラマが特別な操作を行うことなく、整数リテラルを任意精度整数として使用できます。
以下のプログラムは、任意精度階乗関数を実装しています。
カリー化された関数には、冗長なコードの排除など、多くの用途があります。たとえば、モジュールで型の関数が必要な場合でも、型と型のオブジェクト間に固定的な関係がある場合、型の関数を書く方が便利です。型の関数はこの共通性を抽出できます。これはアダプタパターンの例です。a->ba*c->bacc->(a*c->b)->a->b
この例では、与えられた関数の点における数値微分を計算します。fundfx
- fun d delta f x = ( f ( x + delta ) - f ( x - delta )) / ( 2.0 * delta ) val d = fn : real -> ( real -> real ) -> real -> realの型は、「浮動小数点数」を型の関数にマッピングすることを示しています。これにより、カリー化として知られる部分的な引数適用が可能になります。この場合、関数は引数で部分適用することにより特殊化できます。このアルゴリズムを使用する場合の適切な選択肢は、マシンイプシロンの立方根です。fund(real->real)->real->realddeltadelta
- val d' = d 1E~8 ; val d' = fn : ( real -> real ) -> real -> real推論された型は、最初の引数としてd'型を持つ関数を期待していることを示しています。の導関数の近似値を計算できます。real->realで正解は。
- d' ( fn x => x * x * x - x - 1.0 ) 3.0 ; val it = 25.9999996644 : realBasis Library [ 8 ]は標準化されており、ほとんどの実装に同梱されています。ツリー、配列、その他のデータ構造、入出力、システムインターフェースのモジュールを提供します。
数値計算のために、行列モジュールが存在します（ただし、現在は壊れています）。https ://www.cs.cmu.edu/afs/cs/project/pscico/pscico/src/matrix/README.html。
グラフィックスに関しては、cairo-smlはCairoグラフィックスライブラリへのオープンソースインターフェースです。機械学習に関しては、グラフィカルモデル用のライブラリが存在します。
Standard MLの実装には、以下のものが含まれます。
標準
デリバティブ
研究
これらの実装はすべてオープンソースであり、無料で利用できます。そのほとんどはStandard MLで独自に実装されています。現在では商用実装は存在しません。かつてHarlequin社（現在は倒産）がMLWorksという商用IDEとコンパイラを開発していましたが、これはXanalys社に引き継がれ、2013年4月26日にRavenbrook Limited社に買収された後、オープンソース化されました。
コペンハーゲンIT大学のエンタープライズアーキテクチャ全体は、職員記録、給与計算、コース管理とフィードバック、学生プロジェクト管理、Webベースのセルフサービスインターフェースなど、約10万行のSMLで実装されています。[ 9 ]
証明支援システムであるHOL4、Isabelle、LEGO、Twelfは Standard ML で記述されています。コンパイラ開発者やARMなどの集積回路設計者もこれを利用しています。[ 10 ]
Standard MLについて
後継のMLについて
実用的
アカデミック