コンテンツにスキップ

英文维基 | 中文维基 | 日文维基 | 草榴社区

「関数型プログラミング」の版間の差分

出典: フリー百科事典『ウィキペディア(Wikipedia)』
削除された内容 追加された内容
タグ: Refタグつき記述の除去 ビジュアルエディター
46行目: 46行目:
関数型プログラミングの[[型システム]]は、[[型付きラムダ計算]]ベースの[[型理論]]に基づいたスタイルで実装されている。型システムの分類に従った対比で述べると、[[命令型言語]]では明示的型付け(''manifest typing'')が多用されるのに対し、関数型では暗示的型付け(''inferred typing'')が多用される。また関数型では、個別名化した部品から全体を組み上げてその構成内容で全体を識別できるようにする構造的型付け(''structural typing'')よりも、共通名化した部品から全体を組み上げてそれに便宜的タグを付けて全体を識別できるようにする記名的型付け(''nominal typing'')の方がよく用いられる。これはアドホック多相に該当するものであり、実例は[[型クラス]]である。
関数型プログラミングの[[型システム]]は、[[型付きラムダ計算]]ベースの[[型理論]]に基づいたスタイルで実装されている。型システムの分類に従った対比で述べると、[[命令型言語]]では明示的型付け(''manifest typing'')が多用されるのに対し、関数型では暗示的型付け(''inferred typing'')が多用される。また関数型では、個別名化した部品から全体を組み上げてその構成内容で全体を識別できるようにする構造的型付け(''structural typing'')よりも、共通名化した部品から全体を組み上げてそれに便宜的タグを付けて全体を識別できるようにする記名的型付け(''nominal typing'')の方がよく用いられる。これはアドホック多相に該当するものであり、実例は[[型クラス]]である。


関数型初期の[[LISP]]系の[[S式]]は、コンスを実行時に連結するスタイルでデータストラクチャを扱う潜在的型付け(''latent typing'')であり、これは動的型付け(''dynamic typing'')に分類されるものであった。その後のML系を境にして一定の形式を事前に定めた[[静的型付け]](''static typing'')がどちらかと言うと主流になった。その実装の[[代数的データ型]]は、直積と非交和を表現する型構築子の帰納で形成される静的なデータストラクチャであり、パラメトリック多相で総称化された。''Hindley–Milner''型体系は、このパラメトリック多相に完全対応できる型推論機能を提供して強い静的型付けの実装をサポートした。値をメモリ上のビット列ではなく、構造的な代数式と見なすのが関数型プログラミングの特徴である。前者はただのビット列を識別するためにコンパイラがその識別情報を他に持ち、それを参照する為に予め型名を明示(''manifest'')せねばならないが、後者は値自体が識別情報を兼ねているので常時その推論(''inferred'')で型名を識別できる。この時に用いられる[[型推論]]は、代数的データ型のパターンを等価性を審査できる形まで簡約するような型理論に沿った用法だけでなく、ソースコードの前後の文脈までリサーチして型を導き出せるという実用的な機能である。これによって関数型言語での型注釈と型宣言はもっぱら省略される。
関数型初期の[[LISP]]系の[[S式]]は、コンスを実行時に連結するスタイルでデータストラクチャを扱う潜在的型付け(''latent typing'')であり、これは動的型付け(''dynamic typing'')に分類されるものであった。その後のML系を境にして一定の形式を事前に定めた[[静的型付け]](''static typing'')がどちらかと言うと主流になった。その実装の[[代数的データ型]]は、直積と非交和を表現する型構築子の帰納で形成される静的なデータストラクチャであり、パラメトリック多相で総称化された。''Hindley–Milner''型体系は、このパラメトリック多相に完全対応できる型推論機能を提供して強い静的型付けの実装をサポートした。値をメモリ上のビット列ではなく、構造的な代数式と見なすのが関数型プログラミングの特徴である。前者はただのビット列を識別するためにコンパイラがその識別情報を他に持ち、それを参照する為に予め型名を明示(''manifest'')せねばならないが、後者は値自体が識別情報を兼ねているので常時その推論(''inferred'')で型名を識別できる。


[[多態性]]三種の三番目であるサブタイピングは、データのセマンティクスまたは振る舞いの多相を扱う性質から関数型とは相容れない部分が多い。関数型の[[代数的データ型]]とオブジェクト指向の[[抽象データ型]]は対象的なデータストラクチャと見なされている。前者がデータのみの表現体であるのに対して、後者はセマンティクスを主にしたデータの表現体である。しかしオブジェクト指向との連携が模索される中で数々の手法も提示されている。動的型付けメインのLISP系ではS式の代わりに、各スロットに任意の変数を[[動的束縛|動的バインディング]]できるレコードを用いる。その動的束縛用レコードを1個以上引数にできる関数によって[[多重ディスパッチ]]が表現される。動的束縛用レコードの型チェックは[[ダックタイピング]]で行われる。静的型付けメインのML系ではパラメトリック多相を備えた総称化抽象データ型が用いられる。その型引数=型変数には抽象データ型が代入される。関数型プログラミングのサブタイピングは総称化本体の継承関係ではなく、型変数の方の継承関係を用いるのが特徴である。総称化本体のジェネリックインスタンスは型変数の方の継承関係で結ばれる。型変数の派生で結ばたジェネリックインスタンス総称してヴァリアントと呼ばれる。ヴァリアントは型変数の継承関係による仮想関数を提供する。この時にアドホック多相に該当する型境界(''type bound'')で型引数=型変数を修飾させて静的な型チェックをサポートさせる事もある。
[[多態性]]三種の三番目であるサブタイピングは、データのセマンティクスまたは振る舞いの多相を扱う性質から関数型とは相容れない部分が多い。関数型の[[代数的データ型]]とオブジェクト指向の[[抽象データ型]]は対象的なデータストラクチャと見なされている。前者がデータのみの表現体であるのに対して、後者はセマンティクスを主にしたデータの表現体である。しかしオブジェクト指向との連携が模索される中で数々の手法も提示されている。動的型付けメインのLISP系ではS式の代わりに、各スロットに任意の変数を[[動的束縛|動的バインディング]]できるレコードを用いる。その動的束縛用レコードを1個以上引数にできる関数によって[[多重ディスパッチ]]が表現される。動的束縛用レコードの型チェックは[[ダックタイピング]]で行われる。静的型付けメインのML系ではパラメトリック多相を備えた総称化抽象データ型が用いられる。その型引数=型変数には抽象データ型が代入される。関数型プログラミングのサブタイピングは総称化本体の継承関係ではなく、型変数の方の継承関係を用いるのが特徴である。総称化本体のジェネリックインスタンスは型変数の方の継承関係で結ばれる。れはヴァリアントと呼ばれる。ヴァリアントは型変数の継承関係による仮想関数を提供する。この時にアドホック多相に該当する型境界(''type bound'')で型変数を修飾させて静的な型チェックをサポートさせる事もある。


== 歴史 ==
== 歴史 ==
147行目: 147行目:


== 関数型プログラミングの例 ==
== 関数型プログラミングの例 ==
関数型プログラミングは「計算とは何か」という数学の理論を基礎にしており、関数型プログラミングがもつ[[計算モデル]]は'''関数モデル'''である<ref>計算モデル2 関数モデル. (中略) 関数モデルに基づくプログラミング言語. 関数型言語. Lisp [http://nous.web.nitech.ac.jp/individual/inuzuka/lecture/PLT/PLT07/ 犬塚信博 (2007)「プログラミング言語論 第1回 イントロダクション」名古屋工業大学]</ref>。たとえば、1 から 10 までの整数を足し合わせるプログラムを考える{{efn|本来は[[等差数列]]の和の公式を用いて定数時間で問題を解く方法が最適解だが、ここではプログラミングスタイルの比較のため数値計算的手法を用いる。}}。[[命令型プログラミング]]では以下のように[[ループ (プログラミング)|ループ]]文を使って変数に数値を足していく(計算機の状態を書き換える)命令を繰り返し実行するという形を取る。
手続き型言語による[[フィボナッチ数列]]<syntaxhighlight lang="c">

int fibona (int num) {
* [[Pascal]]による例:
int x = 1, y = 1, tmp = 0;
<syntaxhighlight lang="pascal">
for (int i = 2; i < num; i++) {
program test;
tmp = x;
x = y;
var total, i : Integer;
begin
y += tmp;
total := 0;
}
for i := 1 to 10 do
return y;
total := total + i;
}
WriteLn(total)
end.
</syntaxhighlight>
</syntaxhighlight>


一方、関数型プログラミングでは、繰り返しには一時変数およびループを使わず、[[サブルーチン|関数]]の[[再帰呼び出し]]を使う。
関数型言語によるフィボナッチ数列<syntaxhighlight lang="haskell">

let rec fibona num = if num <= 2 then 1 else fibona (num - 1) + fibona (num - 2)
* [[F Sharp|F#]]による例:
<syntaxhighlight lang="fsharp">
printfn "%d" (let rec sum x = if x > 0 then x + sum (x - 1) else 0
sum 10)
</syntaxhighlight>
</syntaxhighlight>
<!--
<!--
171行目: 177行目:
</syntaxhighlight>
</syntaxhighlight>
-->
-->

ただし再帰呼び出しは[[スタックオーバーフロー]]の危険性やオーバーヘッドを伴うため、注意深く使用しなければならない<ref>[https://msdn.microsoft.com/ja-jp/library/dd233229(v=vs.120).aspx 関数 (F#) | MSDN]</ref>。通例、関数型言語では、[[末尾再帰]]呼び出し (tail-recursive call) の形で書かれた関数をループに展開する[[末尾再帰#末尾呼出し最適化|末尾呼出し最適化]]により、スタックオーバーフローの危険性および再帰のオーバーヘッドを解消できる。[[Scheme]]など、関数型言語の中には末尾再帰呼び出しの最適化を仕様で保証するものもある。再帰関数を末尾再帰に書き換えることが難しいケースも有り、そのような場合は一般的なループが採用される。

また、関数型言語は文 (statement) よりも式 (expression) を中心とした言語仕様となっていることも特徴である。前述の例において、再帰関数<code>sum</code>を[[束縛 (情報工学)|束縛]]する<code>let</code>は式である。また、条件分岐の<code>if-then-else</code>も式である。文よりも式で書けることが多いほうが都合がよい。

関数型言語は関数型プログラミングをサポートする言語ではあるが、手続き型プログラミングを行なうことも可能である。例えばF#では以下のようなPascal風の書き方もできる。

<syntaxhighlight lang="fsharp">
let mutable total = 0
for i = 1 to 10 do
total <- total + i
printfn "%d" total
</syntaxhighlight>

ただし[[Haskell]]のようにループ構文をサポートせず、従来の手続き型プログラミングが難しいケースもある。

逆に手続き型言語を使って関数型プログラミングを行なうことも可能であるが、末尾再帰呼び出しの最適化がサポートされるかどうかはコンパイラ次第である。


== 脚注 ==
== 脚注 ==

2020年6月14日 (日) 11:40時点における版

関数型言語: functional language)は、関数型プログラミングのスタイルまたはパラダイムを扱うプログラミング言語の総称である。関数型プログラミングは関数の適用合成から組み立てられる宣言型プログラミングの一形態であり、関数は引数の適用から先行式の評価を後続式の適用に繋げて終端評価に到るツリーとして定義される。関数は引数ないし返値として渡せる第一級関数として扱われる。

関数型プログラミングは数理論理学と代数系をルーツにし、ラムダ計算コンビネータ論理を幹にして構築され、LISP言語が実装面の先駆になっている。関数の数学的な純粋性を指向したものは純粋関数型言語と個別に定義されている。命令型プログラミング言語(手続き型オブジェクト指向を指す)では単に有用な構文スタイルとして扱われている事が多い。高階関数第一級関数関数合成英語版部分適用英語版無名関数クロージャ継続部分関数ポイントフリー英語版パイプラインイテレータジェネレータ代数的データ型型推論パターンマッチングガードパラメトリック多相英語版アドホック多相英語版束縛変数イミュータブル純粋関数英語版などが関数型プログラミングのスタイル要素として挙げられる[誰?]

特徴

ここでは関数型プログラミング本来の構文スタイルを元にして説明する。式を基本文にする関数型に対して、ステートメントを基本文にする命令型プログラミング言語では必要に応じて構文スタイルを変えて実装されている。代表的なのは「式の引数への適用」に対する「引数を関数に渡す」である。値とその型付けに対するコンセプトおよびデータストラクチャの実装スタイルも異なっている。ただし双方ともアセンブリコード上では同様なものに符号化される。

式と関数

関数型プログラムの基本文はexpression)である。式は大まかに言うと値(value)演算子(operator)関数(function)で構成される。値は束縛変数自由変数を包括する。式内の変数部分が特定される前の式は評価できないボトム型存在である。特定後は評価戦略に従ったタイミングで評価(evaluation)されて式存在から値存在になる。式は値と同一視されるので上述の式と値は相互再帰の関係にある。式内の値は他の式の評価値である事があり、その式内にもまた他の値があるといった具合である。この仕組みは高階論理と呼ばれる。

関数も値と同一視される。関数は式に引数を結び付ける機能であり、これは式の引数への適用application)と呼ばれる。式内の仮引数(parameter)箇所に実引数(argument)が順次当てはめられ、式ツリーの終端式が評価値になる。引数によってはボトム型になる関数もありこれは部分関数と呼ばれる。ボトム型は虚(falsity)と見なされており、式のツリーないし写像の連鎖の失敗した終着点になる。関数は、式を第1引数に適用したもの→第x引数に適用したもの→評価値、という形をとる。引数を1個ずつ適用する形態はカリー化と呼ばれる。2個以上の引数を同時適用する形態は非カリー化と呼ばれる。関数の型(function type)は「A→B→C」のように各引数値から評価値までの写像パターンで表現される。片方の評価値と片方の第1引数が同じ型の両関数は任意に連結して新たな関数にできる。この双方の写像のつなぎ合わせは関数合成と呼ばれる。カリー化された関数は引数の適用を途中で止めて残り引数を後から適用するように保留できる。この保留状態の関数の生成は部分適用と呼ばれる。任意のタイミングで遅延評価(call/cc)するために式存在のまま保留中の関数は継続と呼ばれる。その応用に、一つの式を”各変数に各個作用する継続”に分解したものをそれぞれボトムアップで組み上げて一つの継続集合体を生成する継続渡しスタイルがある。関数も当然ながら高階論理に組み込まれている。引数値または評価値として扱うことができる関数は第一級関数と呼ばれる。その第一級関数を扱うことができる関数は高階関数と呼ばれる。

関数は名前付きと名前無しの二通りある。後者はラムダ抽象を模した構文で式中に直接定義される。これは無名関数と呼ばれる。式内に自由変数を持った無名関数はクロージャと個別に定義される。自由変数には外部データが代入される。自身を参照する無名関数を内包したデータ構造体(関数オブジェクト)もクロージャに相当する。無名関数は引数をピュアマッピングする純粋関数である。クロージャの引数のマッピングは式内の自由変数に影響され、またその自由変数に作用する事もあるという副作用要素を閉包した非純粋関数である。関数の名前は、それに結び付けられた式または式ツリーの不動点の表現になる。自式の不動点を式内に置いて新たな引数と共に高階論理の式として評価する手法は再帰と呼ばれる。イミュータブル性が重視されない場合、関数の終端式での再帰は、実引数の更新+先端式へのアドレスジャンプと同等に見なせるので専らそちらに最適化される。これは末尾再帰と呼ばれる。同様の仕組みで相互再帰を最適化した兄弟再帰(sibling recursion)もある。名前付き関数で、仮引数記述を省略したものはポイントフリーと呼ばれ、その省略箇所に先行式評価値が実引数として暗黙適用される。名前無し関数で、先行式評価値を実引数にする記述を省略して、その仮引数箇所に暗黙適用するのもポイントフリーと呼ばれる。この暗黙適用の式を並べて連鎖させる手法はパイプラインと呼ばれるが、言語によっては特別な演算子と併せて明示する。リスト処理時にリストの各要素に対する作用子として渡される第一級関数はイテレータと呼ばれる。作用後の各要素を別の新生リストに向けて複製する働きを加えたものはジェネレータと呼ばれる。これはイミュータブル重視時に多用される。前者はポイントフリーの無名関数、後者はポイントフリーのクロージャとして定義される事が多い。

演算子はデフォルトの式内容を持ち、その引数が単項演算子なら1個、二項演算子なら2個に限定された関数と同義である。部分適用された演算子はセクションと呼ばれる。演算子は任意の型をフックした、又は任意の型にフックさせた再定義および追加定義ができる。前者のフックしたは関数のパターンマッチングと同じ仕組みで、後者のフックさせたは抽象データ型の静的メンバ関数と同じ仕組みで実装される。双方ともアドホック多相に該当するものである。

値とデータストラクチャ

関数型プログラミングの値(value)は、単体値を兼ねたあらゆる多重集合を表わすデータストラクチャ(data structure)として実装される。データストラクチャは型理論的には、型構築子(type constructor)を媒体にした1個以上の型の写像であるが、実例的には型構築子を構造体に見立ててその連結体とイメージした方が分かりやすい。型構築子は基本型と入れ子の型構築子で構成される。基本型は数値、論理値、文字値、文字列を指し、言語毎にprimitive型、proper型、scalar型などと呼ばれる。関数型言語で用いられるデータストラクチャの代表例は代数的データ型S式である。これらは端的に言うと基本型ないし入れ子型構築子のストリーム体であるが、型理論の解釈を加える事でイメージ的に様々な型パターン(pattern)の表現体になる。その型パターンが「型」になり、型パターンの構築が「型付け」になる。値は同時に型パターンの表現体であり、型と値を融合させた型付け値はターム(term)と呼ばれる。

S式は、コンス(cons)と呼ばれる”双子セル”型構築子のみで形成されるデータストラクチャであり、コンスを実行時に連結して任意の型パターンを構築する動的型付けの値である。セルには基本型ないし入れ子コンスが入る。コンスの連結によるセル要素の並びは型理論直積型product type)と見なされる。直積型はタプルのパターンを表わすが、S式では3要素以上のタプルはリストと呼ばれる事が多い。コンスのセルにはあらゆるタームが入れられるので事実上の非交和型sum type)として扱う事もできる。S式は、実行時に文字列を関数名に解釈できる機能を備えているので関数名と引数値をセル要素として並べたタプルをコンスに入れる事もできる。このタプルの遅延評価による値反映は型理論の詳細型(refinement type)に該当する。

代数的データ型は、直積型非交和型を定義できる型構築子の組み合わせで任意の型パターンを構築する静的型付けの値である。トップレベルの型構築子の識別名は同時に新たな代数的データ型の識別名になる。型構築子=代数的データ型は入れ子可能でそのネストは型理論の帰納型(inductive type)とされる。左辺の代数的データ型(自分自身)をネストしたものは再帰データ型recursive data type)とされる。その入れ子と基本型は型パターン内で型変数(type variable)として扱われパラメトリック多相で総称化できる。型構築子は型引数(type parameter)とあわせて定義され総称化された各要素を決定する。代数的データ型はネストされてもその末端は必ず基本型になる。基本型に到るまでの帰納パターンはカインドと呼ばれ代数的データ型の分類基準になる。カインドは「*→*」「*」のように各タームを有効抽象(valid type)にした帰納パターンで表現される。なおカインド判定では同じ構築子への帰納は再帰とされスルーされる。カインドは様々な場面でのパターンマッチの判定基準になる。また型パターンにアドホック多相に該当するアノテーションを直接加えて、元々の等価性に上乗せした任意の用途性で代数的データ型を分類する事ができる。このアノテーションパターンは交差型(intersection type)と呼ばれ、型クラスを表現する。冒頭の、直積型はタプルまたはレコードのパターンを表わす。非交和型は列挙型またはタグ共用体のパターンを表わす。前者は等値性(equality)で識別される一般的な非交和である。後者は等価性(equivalent)で識別される非交和であるが、ユニオン型(union type)と個別定義されてもいる。帰納型と非交和型とユニット型の組み合わせは連結リスト二分木のパターンを表わす。ユニット型(unit type)はnilないしvoidであり空集合のパターンを表わす。ユニット型とそうでない型の二択の非交和型は選択型(option type)と個別に定義され、Maybe値のパターンを表わす。ガードの組み込みによる値反映は詳細型(refinement type)とされ、リスト内包表記のパターンに用いられている。これら上述の各パターンを組み合わせた型パターンがそのまま「型」の表現になり、互いの型パターンが一致する値は等価(equivalent)と見なされる。

パターンマッチング式は、直感的型理論英語版の解釈が適用された広義の代数的データ型である。パターンマッチング式の多分岐写像の評価値は、CASEの式ないし値を依存値にした存在量化子there exists)である。そのパターンマッチ節は等価性または等値性のパターン審査を行い、任意の要素をワイルドカードにした部分的パターン審査もできる。ガード節は等値性または順序性の論理的審査を行う。なお、関数のパターンマッチングはもっぱらアドホック多相の方で解釈される。パターンマッチング式の糖衣構文であるIF-THEN-ELSE式も同様に広義の代数的データ型であるが、こちらはガードの仕組みによる全称量化子for all)である。

評価戦略

関数型プログラミングにおける評価戦略とは「式存在」を「値存在」にする評価タイミングの定義を指す。引数として渡される「存在」を定義するcallbyWhatの方は、関数型の性格上選択肢が限定されるので余り考慮されない。これはまず正格評価(strict evaluation)と非正格評価(non-strict evaluation)の二つに大別される。正格評価の式存在は、関数による適用と同時に評価されて値存在になり、または変数による束縛と同時に評価されて値存在になる。関数の引数節で直積された式存在は理論上全て同時に評価される事になる。その実装は直積された式存在を副作用を伴わずに並行計算するか一つ一つ評価していく事になる。単に一つ一つ評価していくものは先行評価になり、ここでも副作用を伴わない事が原則とされるが必須ではなくなる。正格と先行評価のcallbyWhatは値渡しのみに限定され、参照渡し、複製渡し、共有渡し(アドレス渡し)は当然除外される。代数的データ型では、型構築子への型引数は先行評価対象であり総称化された型変数に宣言と同時に適用される。

後者の非正格評価は遅延評価と慣例上同義に見なされるが、厳密に言うと後者は前者のサブセットである。ただし以降で説明する非正格評価のバリエーションのどれが遅延評価に当たるのかは諸説分かれるので、非正格評価=遅延評価とする方が無難になっている。ここでも遅延評価に統一する。遅延評価のcallbyWhatは名前渡し(式渡し)と必要渡し(メモ化渡し)の二つが有効である。名前渡しによる遅延評価の式存在は、関数に適用されても式存在のままであり、または変数に束縛されても式存在のままである。後続式において改めて他の関数ないし演算子に適用される時に初めて評価されて値存在になり、または改めて他の変数に束縛される時に初めて評価されて値存在になる。これは数理的には束縛項が他の項に束縛された時は必ず簡約化されるという規則に準じたものであり、その簡約化が即ち式評価になる。これが遅延評価のデフォルトタイミングであるが、不評価特殊演算子、継続コール(call/cc)手法、不可反駁(irrefutable)指定などによって更に評価を遅延させる事もできる。継続コールは任意の第一級関数またはクロージャを任意のタイミングで評価して値を導出できる機能である。これは値の導出後も式存在のままなので再利用できる。コール前の部分適用とコール時の引数適用、クロージャの方では自由変数への任意時代入も可能である。不可反駁指定はその式存在の変数部分が不特定でボトム型を導出する場合は評価を取り止め、特定している場合のみに評価を成立させて値存在にする機能である。ただしこれは遅延パターンマッチングで等価性審査から評価値写像につなげる為の内包表記用途にほぼ限定されている。冒頭の必要渡し(メモ化渡し)による遅延評価は参照透過性を忠実履行するものであり、式評価後の値存在は同時にメモ化され、同一の式存在が再び引数にされた時は再評価されずにメモ化された値存在の方を渡すという仕組みである。この強制的な最適化による遅延評価は純粋関数型言語でのみ実装される事になる。代数的データ型では、タグ共用体連結リスト再帰データ型などの式パターンは遅延評価対象であり、これによって無限リストなどの表現が可能になっている。

プログラム実装上において先行評価は一応必須にはならないが、遅延評価の方は必須になる。帰納再帰無限極限といった代数的表現は遅延評価でのみ実装できる。部分関数も遅延評価前提の式存在である。フロー分岐によって参照されなくなる式評価を結果的にスキップできる事は処理の高速化につながる。それはしばしばテクニックとしても用いられる。またボトム型が発生する式評価のスキップはフォールトトレランスにもつながる。ただし柔軟な評価タイミングは同時に式存在と値存在の区別を困難にしてバグの温床になりがちなので、遅延評価が必要になる場所以外では、評価タイミングが明白の先行評価をデフォルトにするのが理想と見なされている。

参照透過性

参照透過性とは関数は同じ引数値に対して必ず同じ評価値を恒久的に導出し、その評価過程において現行計算枠外の情報資源に一切の作用を及ぼさないというプロセス上の枠組みを意味する。現行計算枠外のいずれかの情報資源が変化するのと同時にいずれかの関数の評価過程も変化してしまう現象が副作用と呼ばれる。参照透過性はこの副作用の論理的排除も同時に意味している。参照透過性に則した関数実装は関数の純粋化と呼ばれる。副作用の論理的排除は関数の純粋化の他、あらゆる再代入処理をプログラムから排除する事で成立する。それによってプログラム内に存在するあらゆる値の写像の履歴が、プログラム開始時に宣言(declarative)された初期値まで遡れるようになり、これが参照透過性本来の存在意義になる。再代入処理は自由変数の他、リスト更新、クロージャ、継続、空値スキップ、ボトム型処理、システムコール、各種I/O作業なども指しており、参照透過性を維持しつつそれらを実装するための仕組みが後述の派生構造型であり、モナドである。

宣言(declarative)値からあらゆる存在値を結ぶ膨大な写像の履歴ツリーの解析と模型化は、プロセス微積分ないしプロセス代数と呼ばれ並行プログラミングの支柱にされている。並行プログラミングの基本メカニズムは、全プロセスをまず無制約に並行実行させておき、どこかで不整合(conflict)が発生した場合は一定の関連プロセスを整合性が取れる履歴ツリー上の写像位置まで巻き戻すというものである。過去に戻ったプロセスは不整合が反映された別の写像ルートを辿ることになるが、そのルート変化は未来情報の反映になるので副作用には当たらない。この時に履歴ツリーが用いられる。従って写像履歴の改ざんにつながる再代入処理は厳禁になり、代わりにある時点の写像をただ書き留めておく束縛変数と、旧値の更新を新値の産出で代替したイミュータブル、そして前述の副作用を論理的に排除する派生構造型ないしモナドが不可欠になる。ループは関数の再帰で行われ、条件分岐は直感的型理論の解釈が適用された代数的データ型で表現される。

また参照透過性で有効になる写像の履歴ツリーは、一定の証明論に基づいたプルーフアシスタントによるプログラム正当性の自動的な形式的検証および数学的証明を可能にする。プルーフアシスタントはソフトウェアツールである。純粋関数型言語はその為に参照透過性をプログラム全体の枠組みにしている。プログラム全体に参照透過性を適用するには関数の純粋化と再代入処理の排除の他に、プログラムレベルでは回避できない各種I/O作業に伴う必然的副作用の論理的排除も必要になるので専用のランタイム環境上での動作が必須になる。ランタイム環境は「コンテキスト」を走行プログラムとの仲介にする。プログラム内の各関数は、ライナー型引数値として渡されたコンテキストに作用するという形で各種I/O作業を行う。その仮想的I/O作業はランタイム環境側で実際に代行され、そのI/O作業で変化したコンピュータ環境はその都度コンテキストに反映される。関数はコンテキストをライナー型返り値として渡し返す。ライナ―型(linear type)は型理論における派生構造型(substructural type)の一形態であり線形合同法に似たデータ生成アルゴリズムによる写像履歴を維持するための型システムである。これはユニークネス型とも呼ばれる。コンテキストに「関連値」を注入する仕組みはアフィン型(affine type)、抽出する仕組みは関連型(relevant type)と呼ばれる。双方とも派生構造型の一形態である。このように各種I/O作業をコンテキストへの作用という形にする事で副作用を論理的に排除し、ライナー型の疑似乱数列に似た仕組みで参照透過性を論理的に維持している。常にユニーク生産されるライナー型値は、I/O作業の副作用によって実際には変化しているランタイム環境の時系列状態を完全に抽象化して、それらを理論上各個照会可能にしているマッピングキーである。これによってランタイム環境の変化も写像の履歴ツリーで論理的に辿れるようにしている。なお、型システムの代わりに圏論を利用して写像履歴を維持するためのデザインパターン手法がモナドである。コンテキストに作用するモナド演算子は数学問題における公理公式と同等の存在であり、決められたルールに従って用いるだけで副作用の排除と参照透過性の維持を論理的に表現できる。

型システム

関数型プログラミングの型システムは、型付きラムダ計算ベースの型理論に基づいたスタイルで実装されている。型システムの分類に従った対比で述べると、命令型言語では明示的型付け(manifest typing)が多用されるのに対し、関数型では暗示的型付け(inferred typing)が多用される。また関数型では、個別名化した部品から全体を組み上げてその構成内容で全体を識別できるようにする構造的型付け(structural typing)よりも、共通名化した部品から全体を組み上げてそれに便宜的タグを付けて全体を識別できるようにする記名的型付け(nominal typing)の方がよく用いられる。これはアドホック多相に該当するものであり、実例は型クラスである。

関数型初期のLISP系のS式は、コンスを実行時に連結するスタイルでデータストラクチャを扱う潜在的型付け(latent typing)であり、これは動的型付け(dynamic typing)に分類されるものであった。その後のML系を境にして一定の形式を事前に定めた静的型付けstatic typing)がどちらかと言うと主流になった。その実装の代数的データ型は、直積と非交和を表現する型構築子の帰納で形成される静的なデータストラクチャであり、パラメトリック多相で総称化された。Hindley–Milner型体系は、このパラメトリック多相に完全対応できる型推論機能を提供して強い静的型付けの実装をサポートした。値をメモリ上のビット列ではなく、構造的な代数式と見なすのが関数型プログラミングの特徴である。前者はただのビット列を識別するためにコンパイラがその識別情報を他に持ち、それを参照する為に予め型名を明示(manifest)せねばならないが、後者は値自体が識別情報を兼ねているので常時その推論(inferred)で型名を識別できる。

多態性三種の三番目であるサブタイピングは、データのセマンティクスまたは振る舞いの多相を扱う性質から関数型とは相容れない部分が多い。関数型の代数的データ型とオブジェクト指向の抽象データ型は対象的なデータストラクチャと見なされている。前者がデータのみの表現体であるのに対して、後者はセマンティクスを主にしたデータの表現体である。しかしオブジェクト指向との連携が模索される中で数々の手法も提示されている。動的型付けメインのLISP系ではS式の代わりに、各スロットに任意の変数を動的バインディングできるレコードを用いる。その動的束縛用レコードを1個以上引数にできる関数によって多重ディスパッチが表現される。動的束縛用レコードの型チェックはダックタイピングで行われる。静的型付けメインのML系ではパラメトリック多相を備えた総称化抽象データ型が用いられる。その型引数=型変数には抽象データ型が代入される。関数型プログラミングのサブタイピングは総称化本体の継承関係ではなく、型変数の方の継承関係を用いるのが特徴である。総称化本体のジェネリックインスタンスは型変数の方の継承関係で結ばれる。これはヴァリアントと呼ばれる。ヴァリアントは型変数の継承関係による仮想関数を提供する。この時にアドホック多相に該当する型境界(type bound)で型変数を修飾させて静的な型チェックをサポートさせる事もある。

歴史

1930年代に数学者アロンゾ・チャーチによって発明されたラムダ計算関数適用をベースにした計算用形式体系であり、1937年に数学者アラン・チューリング自身によりチューリング完全の性質が明らかにされて、チューリングマシンと等価な計算模型である事が証明されている。この経緯からラムダ計算は関数型プログラミングの基底に据えられた。ラムダ計算と同等の計算理論コンビネータ論理があり、1920年代から1930年代にかけて数学者ハスケル・カリーらによって発明されている。こちらは関数型プログラミングの原点である高階論理式の基礎モデルにされた。チャーチはラムダ計算を拡張してその各タームに型を付与した型付けラムダ計算も考案しており、これは関数型プログラミングにおける型理論型システムの源流になった。

1950年代

初の関数型プログラミング言語とされる「LISP」は、1958年にマサチューセッツ工科大学の計算機科学者ジョン・マッカーシーによって開発された。LISPの関数はラムダ計算の形式を元に定義され再帰可能に拡張されており、式のリスト化とその遅延評価および高階評価など幾つかの関数型的特徴を備えていた。LISPは数多くの”方言”を生み出しているが、その中でも「Scheme」「Dylan」「Racket」「Clojure」「Julia」は取り分け関数型の特徴を明確にした言語である。1956年に公開された「Information Processing Language」の方が先駆であるが、こちらはアセンブリベースの低水準言語なので前段階扱いである。IPLが備えていたニーモニックコードのリストをオペランドにできるジェネレータ機能はLISPに影響を与えたと言われる。高階オペランドの演算処理は高階関数と同じ働きをし、メモリ一括処理のストリング命令の効率を高めるなどした。

1960年代

1964年に計算機科学者ケネス・アイバーソンが開発した「APL」は、数多く定義された関数記号を多次元配列データに適用する機能を中心にした言語であり、取り分けスプレッドシート処理に対する効率性が見出されて、1960年代以降の商業分野と産業分野に積極導入された。APLは関数型ではなく配列プログラミング型に位置付けられているが、配列を始めとするデータ集合に対する関数適用の有用性を特に証明した言語になった。そのデータ集合処理の可能性に注目した「J」「K」「Q」といった派生言語が後年に登場している。続く1966年に発表された「ISWIM」は関数型を有用な構文スタイルとして扱うマルチパラダイム言語の原点とされ、ALGOLを参考にした構造化プログラミングに高階関数とwhereスコープが加えられていた。60年代の関数型プログラミングの歴史はもっぱらLISPの発展を中心にしていたが、ISWIMは後年の「ML」「Scheme」のモデルにされている。

1970年代

相互自動定理証明に向けて始められた「Logic for computable functions」プロジェクトの中で1973年に導入された「ML」は代数的データ型パラメトリック多相型推論などを備えた関数型言語であり、計算機科学者ロビン・ミルナーによって開発された。また1975年にMIT人工知能研究所の計算機科学者ガイ・スティールと工学者ジェイ・サスマンが設計してAIリサーチ用に導入された「Scheme」は任意時評価(call/cc)第一級継続などを備え、レキシカルスコープで構造化が図られており末尾再帰を最適化していた。MLとScheme双方の登場は関数型プログラミングのマイルストーンになった。また同年代に代数的データ型を初めて導入しクリーネの再帰定理を証明実装した「Hope」と、関数の数学的純粋性を初めて重視した「SASL」も発表されている。1977年、バッカス・ナウア記法FORTRAN開発の功績でこの年のチューリング賞を受けた計算機科学者ジョン・バッカスは「Can Programming Be Liberated From the von Neumann Style? -A Functional Style and Its Algebra of Programs-」と題した記念講演を行い、一説にはこれを境にして関数型(functional)というパラダイム名が定着したと言われる。なお同時に発表された「FP」は関数水準(function-level)言語として紹介されている。バッカスはFPのプログラムをアトム+関数+フォーム(=高階関数)の階層構造と定義し、代数を用いるフォームの結合で全体構築されると提唱した。ノイマン型からの脱却を題目に掲げているバッカスの理論は、後年のCPUに導入される並列パイプライン処理に通じる構想であった。

1980年代

1978年にMLの開発者ミルナーが発表した型推論アルゴリズムが1982年に証明されると、パラメトリック多相の柔軟な解釈と併せて値のほぼ確実な等価性審査が可能になった型推論を眼目にするHindley–Milner型体系が確立され、関数型プログラミングの型システムは一つの完成水準に達した。1983年にMLを標準化する目的の下でHindley–Milner型体系を導入した「Standard ML」が発表された。続く1985年にML派生言語の代表格「Caml」が公開された。同じく1985年にSASLの後継として発表された「Miranda」は、遅延評価を標準にしながら関数の数学的純粋性を追求した言語であり、関数型プログラミング研究用オープンスタンダードのコンセンサスで1987年から策定が開始されたHaskellのモデルになりその進捗を大きく後押しした。それと前後してMirandaは1987年公開の純粋関数型言語「Clean」にも大きな影響を与えている。Cleanは後発のHaskellをも叩き台にして改良を続けた。また関数型と並行計算の適性が認識される中で1986年の通信業界で開発された「Erlang」は並行プログラミング指向の面で特に注目を集めている言語である。1988年公開の「Wolfram」はAPLスタイルのリスト処理に強力なパターンマッチングやイテレーションを加えた言語で90年代を通して改良が続けられていた。

1990年代

1990年にこれも関数型プログラミングのマイルストーン的な純粋関数型言語「Haskell」が初リリースされた。1992年に動的型付けレコードクラスと多重ディスパッチメソッドを扱う関数型言語「Dylan」が登場した。1993年にベクトル行列表テーブルなどのデータストラクチャを扱えて統計的検定時系列分析クラスタリング分野に特化した関数型言語「R」が発表された。1995年にLISPのマクロ機能を大幅に強化したコンポーネント指向により各分野に合わせたドメイン固有言語として振る舞える「Racket」が登場した。1996年にはML系列のCamlにオブジェクト指向視点の抽象データ型を導入した「OCaml」が公開された。90年代の関数型プログラミングの歴史では、関数の数学的純粋さを追求する参照透過性指向とオブジェクト指向との連携が比較的目立っていた。日本ではStandard MLに独自の拡張を施した「SML#」が発表されている。風変りなものにコンビネータ論理の形式に立ち返った「Unlambda」がある。論理型プログラミングとの親和性も見直されるようになり、1995年に「Mercury」が公開された。論理型のルール&ファクトのパラダイムはデータ集合に対するフィルタリングなどに活用された。

2000年代

2000年代になると関数型プログラミングへの注目度は更に高まり、マルチパラダイムに応用された関数型言語が様々に登場した。2003年のJava仮想マシン動作でオブジェクト指向と関数型を融合した「Scala」、2005年のマイクロソフト製のML派生言語「F#」、2007年のJava仮想マシン動作のLISP方言「Clojure」など数々のポピュラー言語が生み出されている。また直感的型理論とカリー=ハワード同型対応の理論に基づいたプルーフアシスタント(Proof assistant)によるプログラム正当性の数学的証明を指向した関数型言語が支持され、2004年に「Epigram」2007年に「Agda」および純粋関数型「Idris」が発表されている。これらの言語では型理論依存型も正式に導入されて一歩進んだ型システムを実現している。関数型構文の有用性がより広く認識されるに従い、オブジェクト指向言語やスクリプト言語にも積極的に導入されるようになった。産業分野からも注目されるようになり、CSG幾何フレームワーク上で動くCADへの導入も始められた。しかし関数型コンセプトに馴染まないオペレーターが定数化規則による値の再代入制限に困惑して設計作業に支障をきたすなどの弊害も明らかになっている。

代表的な関数型言語

LISP (1958年)

動的型付け、先行評価

ISWIM (1966年)← LISP、ALGOL

静的型付け

ML (1973年)← ISWIM

静的型付け、先行評価

Scheme (1975年)← LISP、ISWIM

LISP方言、動的型付け、先行評価

FP (1977年)

純粋

Standard ML (1983年)← ML、Hope、PASCAL

ML派生、静的型付け、先行評価

Miranda (1985年)← ML、SASL、Hope

純粋、静的型付け、遅延評価

Erlang (1986年)← LISP、PrologSmalltalk

動的型付け

Clean (1987年)← Miranda

純粋、静的型付け、遅延評価

Haskell (1990年)← ML、Scheme、Miranda、Clean、FP

純粋、静的型付け、遅延評価

Dylan (1993年)← Scheme、CLOSALGOL

LISP方言、動的型付け、先行評価

R (1993年)← Scheme、CLOS

動的型付け、先行評価

Racket (1995年)← Scheme、Eiffel

LISP方言、動的型付け、先行評価

OCaml (1996年)← Caml、Standard ML、Modula-3

ML派生、静的型付け、先行評価

Scala (2003年)← Scheme、Haskell、OCaml、Erlang、SmalltalkJava

静的型付け、先行評価

F# (2005年)← Haskell、OCaml、Erlang、Scala、PythonC♯

ML派生、静的型付け、先行評価

Clojure (2007年)← Scheme、Haskell、OCaml、Erlang、Java

LISP方言、動的型付け、先行評価

関数型プログラミングの例

関数型プログラミングは「計算とは何か」という数学の理論を基礎にしており、関数型プログラミングがもつ計算モデル関数モデルである[1]。たとえば、1 から 10 までの整数を足し合わせるプログラムを考える[注釈 1]命令型プログラミングでは以下のようにループ文を使って変数に数値を足していく(計算機の状態を書き換える)命令を繰り返し実行するという形を取る。

program test;
var total, i : Integer;
begin
total := 0;
for i := 1 to 10 do
    total := total + i;
WriteLn(total)
end.

一方、関数型プログラミングでは、繰り返しには一時変数およびループを使わず、関数再帰呼び出しを使う。

  • F#による例:
printfn "%d" (let rec sum x = if x > 0 then x + sum (x - 1) else 0
              sum 10)

ただし再帰呼び出しはスタックオーバーフローの危険性やオーバーヘッドを伴うため、注意深く使用しなければならない[2]。通例、関数型言語では、末尾再帰呼び出し (tail-recursive call) の形で書かれた関数をループに展開する末尾呼出し最適化により、スタックオーバーフローの危険性および再帰のオーバーヘッドを解消できる。Schemeなど、関数型言語の中には末尾再帰呼び出しの最適化を仕様で保証するものもある。再帰関数を末尾再帰に書き換えることが難しいケースも有り、そのような場合は一般的なループが採用される。

また、関数型言語は文 (statement) よりも式 (expression) を中心とした言語仕様となっていることも特徴である。前述の例において、再帰関数sum束縛するletは式である。また、条件分岐のif-then-elseも式である。文よりも式で書けることが多いほうが都合がよい。

関数型言語は関数型プログラミングをサポートする言語ではあるが、手続き型プログラミングを行なうことも可能である。例えばF#では以下のようなPascal風の書き方もできる。

let mutable total = 0
for i = 1 to 10 do
    total <- total + i
printfn "%d" total

ただしHaskellのようにループ構文をサポートせず、従来の手続き型プログラミングが難しいケースもある。

逆に手続き型言語を使って関数型プログラミングを行なうことも可能であるが、末尾再帰呼び出しの最適化がサポートされるかどうかはコンパイラ次第である。

脚注

注釈

  1. ^ 本来は等差数列の和の公式を用いて定数時間で問題を解く方法が最適解だが、ここではプログラミングスタイルの比較のため数値計算的手法を用いる。

出典

  1. ^ 計算モデル2 関数モデル. (中略) 関数モデルに基づくプログラミング言語. 関数型言語. Lisp 犬塚信博 (2007)「プログラミング言語論 第1回 イントロダクション」名古屋工業大学
  2. ^ 関数 (F#) | MSDN

外部リンク