関数型プログラミング

関数型言語（英: functional language）は、関数型プログラミングのスタイルまたはパラダイムを扱うプログラミング言語の総称である。関数型プログラミングは関数の適用をベースにした宣言型プログラミングの一形態であり、関数は引数の適用から先行式の評価を後続式の適用につなげて終端の評価を導き出す式のツリー構造として定義される。式の評価に伴う副作用の発生には大きな注意が払われる。関数は引数ないし返り値として渡せる第一級オブジェクトとして扱われる。

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

特徴

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

式と関数

関数型プログラムの基本文は式（expression）である。式は個体である値（value）と写像である関数（function）の二つから構成される。関数の定義には演算子（operator）も含まれている。値は基本データ型（プリミティブ）と複合データ型（コンポジット）およびラムダ計算で言われる変数（variable）を意味する。変数は束縛変数と自由変数を指す。評価（evaluation）される前の式は、ラムダ計算で言われるネーム（name）と同義になる。ネームは数学上の数式または代数式に相当するものである。式は、式内の変数部分が確定される前は評価できないボトム型であり、これはラムダ抽象（abstraction）と同義である。式内の変数部分を確定するのはラムダ適用（application）と同義である。このネームが評価されると値になり、これはラムダ計算で言われる簡約（reduction）と同義である。式は値と同一視されるので、すなわち式と値は相互再帰の関係にある。式内の値は他の式の評価値である事があり、その式内にもまた他の値があるといった具合である。この仕組みは高階論理と呼ばれる。

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

関数は名前付きと名前無しの二通りある。名前無しの関数は専らラムダ抽象を模した構文で定義される。式内に自由変数を内包しない方は無名関数と呼ばれ、自由変数を内包する方はそれを囲い込むという意味でクロージャと呼ばれる。自由変数は外部データへの接点になる。無名関数は引数をピュアマッピングする純粋関数である。クロージャの引数のマッピングは式内の自由変数に影響され、またその自由変数に作用する事もあるという副作用要素を閉包した非純粋関数である。関数の名前は、それに結び付けられた式または式ツリーの不動点の表現になる。自式の不動点を式内に置いて新たな引数と共に高階論理の式として評価する手法は再帰と呼ばれる。関数の終端式での再帰は実引数の更新＋先端式へのアドレスジャンプと同等に見なせるのでもっぱらそちらに最適化されてこれは末尾再帰と呼ばれる。末尾再帰は論理性を損なわずにスタック資源から離れた無制限ループを可能にする実装概念として重視されている。名前付き関数で、仮引数記述を省略したものはポイントフリーと呼ばれ、その省略箇所に先行式評価値が実引数として暗黙適用される。名前無し関数で、先行式評価値を実引数にする記述を省略して、その仮引数箇所に暗黙適用するのもポイントフリーと呼ばれる。この暗黙適用の式を並べて連鎖させる手法はパイプラインと呼ばれるが、言語によっては特別な演算子と併せて明示する。リスト処理時にリストの各要素への作用子として渡される第一級関数はイテレータと呼ばれる。同様にリスト処理時に渡されて各要素を参照しながらそれらの総和値または選別リストまたは更新リストを生成する方はジェネレータと呼ばれる。これはイミュータブル重視時に多用される。イテレータとジェネレータはポイントフリーの無名関数として定義される事が多い。関数名は関手の識別子と同義なので、同じ識別子にそれぞれ異なる引数パターン候補を付けたものを列挙することで選言の関係でつなげる事ができる。これは関数のパターンマッチングと呼ばれる。パターンマッチングは等値性（equality）の照合、ワイルドカードを用いた部分的照合、制約（constraint）またはガードに相当する比較照合と範囲照合、型を意味する等価性（equivalent）の照合などで行われる。演算子はデフォルトの式内容を持ち、その引数が単項演算子なら1個、二項演算子なら2個に限定された関数と同義である。引数を部分適用された演算子はセクションと呼ばれる。演算子もそれぞれ異なる引数パターン候補を付けたものを列挙して選言の関係でつなげる事ができる。これは演算子のパターンマッチングと呼ばれる。

値とデータストラクチャ

関数型プログラミングの値（value）は、基本データ型（プリミティブ）と複合データ型（コンポジット）のいずれかで表現される。プリミティブは数値、論理値、文字値、文字列を指す。様々なプリミティブを様々な形式で組み合わせたものがコンポジットであり、その例はC言語の構造体や共用体などである。その組み合わせ方に焦点を当てた用語がデータストラクチャ（data structure）である。データストラクチャという概念には入れ子構造、再帰構造、木構造、ハッシュ構造、グラフ構造、注釈構造、操作的意味構造といった様々な暗黙情報を含められるので、コンポジットの具体的形式といった意味で用いられる。関数型言語で用いられるデータストラクチャの代表は代数的データ型とS式である。双方とも型構築子（type constructor）から構築される。まず、プリミティブが型構築子によってまとめられる。正確ではないが型構築子はC言語の構造体または共用体と同じものと見てよい。型構築子は入れ子にできるので、型構築子をまとめた型構築子を定義できる。自分自身（型構築子）を入れ子にした再帰構造も定義できる。プリミティブと型構築子を任意に組み合わせて代数的データ型やS式といったデータストラクチャが構築される。データストラクチャ内のプリミティブと型構築子の組み合わせ方はパターン（pattern）と呼ばれる。パターンにはアノテーション要素やガード要素が加えられることもある。そのパターンが型になり、パターンの構築が型付けになり、パターンを量化（quantify）すると型付け値になり、これはターム（term）と呼ばれる。タームは冒頭の値（value）を指す。型構築子のパターンの末端は必ずプリミティブになるので、パターン内の全てのプリミティブの値を決定することが量化になる。特定の文脈が求めるパターンにマッチするタームは等価（equivalent）とされる。この等価は同じ型と読み替えてもよい。等価性はあらゆる計算の可否（計算可能性）を決定する。計算とは関数適用または演算子適用を指し、それらが求める仮引数と実引数にするタームが等価であればその計算は成立する事になる。データストラクチャのパターンは基礎パターンに分解されて解釈される。基礎パターンは型理論に従って直積型、非交和型、帰納型、ユニット型、ユニオン型、オプション型、詳細型、交差型などに分類されている。

S式は二分木構造のデータストラクチャである。これはコンス（cons）と呼ばれる二項の型構築子の連結で形成される。コンスは二つの要素を持つものであり、要素はプリミティブまたは他のコンスのどちらかである。S式はコンスを実行時に連結して任意のパターンを構築する動的型付けの値である。コンスの連結による要素の並びは直積型（product type）となる。直積型はタプルのパターンを表わすが、三要素以上の並びはコンスの連結になるのでリストと呼ばれる。コンスの要素はあらゆるプリミティブと入れ子コンスにできるので形式化されていない非交和型（sum type）でもある。ただしその判別は完全にプログラマ側の裁量に委ねられている。

代数的データ型はAND-OR木構造のデータストラクチャである。これは直積型または非交和型を表現する多項の型構築子の組み合わせで形成される。型構築子は任意個数の要素を持つものであり、要素はプリミティブまたは他の構築子のどちらかである。代数的データ型は型構築子を事前に組成定義して任意のパターンを構築する静的型付けの値である。直積型はタプルまたはレコードのパターンを表わす。非交和型は列挙型またはタグ共用体のパターンを表わす。前者は等値性（equality）で識別される一般的な非交和である。後者は等価性（equivalent）で識別される非交和であるが、ユニオン型（union type）と個別定義されてもいる。自分自身の型構築子のネスティングは型理論の帰納型（inductive type）とされる。非交和型と帰納型とユニット型の組み合わせは連結リストや二分木のパターンを表わす。ユニット型（unit type）はnilないしvoidであり空集合のパターンを表わす。ユニット型とそうでない型の二択の非交和型はオプション型（option type）とされMaybe値のパターンを表わす。代数的データ型を述語論理の関数記号で包含（comprehension）したパターンは詳細型（refinement type）とされる。これは「ターム集合→ガード→抽出タームリスト」のリスト内包表記である。パターンにアノテーションを加えてそれが表わす任意の意味づけ性との論理積で新たな等価性を表現するのは交差型（intersection type）とされ型クラスを表わす。これはアドホック多相に相当する。パターン内のプリミティブと型構築子は、型変数（type variable）に置き換えることでジェネリック化でき、型引数（type parameter）の指定でスペシフィック化できる。これはパラメトリック多相に相当する。代数的データ型は定義と実装を分けて後者を隠蔽するという意味でしばしば抽象化される。これは識別名を重複させる仕組みで実現され、型シノニムまたは型エイリアスと呼ばれる。

評価戦略

関数型プログラミングの評価戦略（evaluation strategy）は、ネーム存在を値存在にする評価タイミング、引数の渡し方のcall-by-What、関数のボトム型の発生タイミングの三つを定義している。これはまず正格評価（strict evaluation）と非正格評価（non-strict evaluation）の二つに大別される。正格評価のネーム存在は、関数適用と同時に評価されて値存在になり、または変数による束縛と同時に評価されて値存在になる。この評価タイミングに注目した方は先行評価（eager evaluation）と呼ばれる。引数のどれか一つがボトム型の値存在になった関数は反駁（refutable）されてそのままボトム型になる。この意味も包括した呼称が正格評価である。正格評価＝先行評価のcall-by-Whatは値渡しになる。関数型プログラミングの性格から参照渡しと共有渡し（ポインタ渡し）は用いられない。

非正格評価の評価タイミングに注目した方は遅延評価（lazy evaluation）と呼ばれる。非正格評価＝遅延評価のcall-by-Whatは名前渡し（ネーム渡し）または必要渡し（メモ化渡し）が用いられる。名前渡しによる遅延評価のネーム存在は、関数に適用されてもネーム存在のままであり、または変数に束縛されてもネーム存在のままである。後続式において改めて他の関数ないし演算子に適用される時に初めて評価されて値存在になり、または改めて他の変数に束縛される時に初めて評価されて値存在になる。これは数理的には束縛項が他の項に束縛された時は必ず簡約化されるという規則に準じている。評価の遅延により、ボトム型になる引数があってもそれが確定するまでは関数が反駁されないという意味も包括した呼称が非正格評価である。これが遅延評価のデフォルトタイミングであるが、継続コール（call/cc）手法や不可反駁（irrefutable）指定によって更に評価を遅延させる事もできる。継続コールは任意の第一級関数またはクロージャを任意のタイミングで評価して値を導出できる機能である。これは値の導出後もネーム存在のままなので再利用できる。コール前の部分適用とコール時の引数適用、クロージャの方では自由変数への任意時代入も可能である。不可反駁指定はそのネーム存在の変数部分が不特定でボトム型を導出する場合は評価を取り止め、特定している場合のみに評価を成立させて値存在にする機能である。ただしこれは遅延パターンマッチングで等価性審査から評価値写像につなげる為の用途にほぼ限定されている。必要渡し（メモ化渡し）による遅延評価は参照透過性を忠実履行するものであり、ネーム存在評価後の値存在は同時にメモ化されて、同一のネーム存在が再び引数にされた時は再評価されずにメモ化された値存在の方を渡すという仕組みである。この強制的な最適化による遅延評価は純粋関数型言語でのみ実装される事になる。評価の遅延は、帰納、再帰、無限、極限といった代数的表現の実装を可能にする。フロー分岐によって参照されなくなる式評価を結果的にスキップできることは処理の高速化につながり、しばしばテクニックとしても用いられる。またボトム型が発生する式評価のスキップはフォールトトレランスにもつながる。ただし柔軟な評価タイミングは同時にネーム存在と値存在の区別を困難にしてバグの温床になりがちなので、遅延評価が必要になる場所以外では、評価タイミングが明白の先行評価をデフォルトにするのが理想またはスタンダードとされている。代数的データ型ではタグ共用体、連結リスト、再帰データ型の構造は遅延評価対象である。連結リストは無限リストと構造上同義である。

参照透過性

参照透過性（referential transparency）とは関数は同じ引数値に対して必ず同じ評価値を恒久的に導出し、その評価過程において現行計算枠外の情報資源に一切の作用を及ぼさないというプロセス上の枠組みを意味する。現行計算枠外のいずれかの情報資源が変化するのと同時にいずれかの関数の評価過程も変化してしまう現象が副作用と呼ばれる。参照透過性はこの副作用の論理的排除も同時に意味している。参照透過性に則した関数実装は関数の純粋化と呼ばれる。副作用の論理的排除は関数の純粋化の他、あらゆる再代入処理をプログラムから排除する事で成立する。それによってプログラム内に存在するあらゆる個体（値）の写像（関数）によるつながりが有向グラフ化されて、プログラム開始時に宣言（declarative）された初期値まで遡れるようになる。宣言値からあらゆる存在値をつなぐ言わば写像の履歴の図表であるプロセス有向グラフの解析と模型化は、プロセス微積分ないしプロセス代数と呼ばれ並行プログラミングなどの支柱になる。関数型プログラミングの世界で再代入がタブーとされるのは、それが写像の履歴の改ざんにつながるからである。従ってある時点の写像をただ書き留めておく束縛変数と、旧値の更新を新値の産出で代替したイミュータブルが重視される。制御フローの反復（ループ）は関数の再帰で表現され、選択（分岐）は非交和の関係でつなげた写像で表現される。再代入処理は自由変数の他、リスト更新、クロージャ、継続、オプション型生成、ボトム型処理、システムコール、各種I/O作業なども指しており、参照透過性を維持しつつそれらを実装するための仕組みが型理論由来の派生構造型であり、圏論由来のモナドである。

参照透過性が保証されたプロセス有向グラフは、一定の証明論に基づいたプルーフアシスタント（proof asistant）によるプログラム正当性の形式的検証および数学的証明を可能にする。純粋関数型言語はその為に参照透過性をプログラム全体の枠組みにしている。プログラム全体に参照透過性を適用するには関数の純粋化と再代入処理の排除の他に、プログラムレベルでは回避できない各種I/O作業に伴う必然的副作用の論理的排除も必要になるので専用のランタイム環境上での動作が必須になる。ここでの論理的とは公理的意味論に沿った正当性を意味する。ランタイム環境は「コンテキスト」を走行プログラムとの仲介にする。プログラム内の各関数は、ライナー型引数値として渡されたコンテキストに作用するという形で各種I/O作業を行う。その仮想的I/O作業はランタイム環境側で実際に代行され、そのI/O作業で変化したコンピュータ環境はその都度コンテキストに反映される。関数はコンテキストをライナー型返り値として渡し返す。ライナ―型（linear type）は型理論の派生構造型（substructural type）の一形態であり、線形合同法に似たユニーク値生成アルゴリズムによってプロセス有向グラフの正当性を維持するための型システムである。これはユニークネス型とも呼ばれる。コンテキストに「関連値」を注入する仕組みはアフィン型（affine type）、抽出する仕組みは関連型（relevant type）と呼ばれる。双方とも派生構造型の一形態である。このように各種I/O作業をコンテキストへの作用という形にする事で副作用を論理的に排除し、ライナー型の疑似乱数列に似た仕組みで参照透過性を論理的に維持している。常にユニークな値に生成されるライナー型値は、I/O作業の副作用によって実際には変化しているランタイム環境の時系列状態を完全に抽象化して、それらを理論上各個照会可能にしているマッピングキーである。これによってランタイム環境の変化もプロセス有向グラフで論理的に辿れるようにしている。なお、型理論の代わりに圏論に基づいてプロセス有向グラフの正当性を維持するための手法がモナドである。参照透過性を維持する以上の機能を持たない派生構造型に対して、モナドの方は関連値とコンテキストの連携を高度に柔軟化して様々に応用可能にした計算の構造化手法であり、その中の共変性を軸にした仕組みにライナー型が注入されて参照透過性の維持を実現している。

型システム

関数型プログラミングの型システム（type system）は、型付けラムダ計算ベースの型理論に基づいたスタイルで実装されている。型システムの分類に従った対比で述べると関数型では、性質や役割による意味づけによって値を分類する明示的型付け（manifest typing）よりも、計算可能性に基づく等価性によって値を分類する推論的型付け（inferred typing）が多用される。前者の意味づけとはプログラマによる型定義、型宣言、型注釈を指しており人間寄りの視点である。後者の等価性とは値を関数または演算子に適用できるかどうかの判別を指し、値への関心がそこで計算可能かどうかに絞られているので計算機寄りの視点である。明示的型付けではソースコード上の型宣言と型注釈から値の型が特定されるのに対し、推論的型付けでは型推論機能で特定される。型推論とはソースコードの解析によって値それぞれの等価性を導き出す機能である。数値や文字列といったリテラルはそのまま特定され、変数などのシンボルはその扱われ方や各等式を並べた任意の法則の定義によって型（=等価性）が特定されるといった具合である。推論的型付けでは値への関心をその計算可能性に絞っているので、型宣言と型注釈は必要とされなくなる。例としてint型を型シノニムで金額型と数量型にした場合、明示的型付けではこの両者は区別されるが、推論的型付けでは区別されない。ソースコードの解析でどちらもint型準拠の等価と見られるからである。ただし型注釈を強制すれば区別されるので等価性と意味づけ性を使い分けられる。型注釈無しのままで値の意味づけ性も表現する場合は、型構築子で値を包むボックス化に似た手法が用いられる。また関数型では、所属する部品に注目して全体を識別する構造的型付け（structural typing）よりも、記名から全体を識別しその文脈で所属する部品も識別する記名的型付け（nominal typing）の方がよく用いられる。その実例は型クラスでありこれはアドホック多相とも言われる。型クラスは型理論における文脈を形式化したものでインターフェースのように用いられる。

関数型初期のLISP系のS式は、二項型構築子（コンス）の実行時の連結で形式化されていないパターンを構築し、プログラマの裁量による実行時の逐次チェックでパターン（型）の意味づけと計算に用いるための等価性を判別するといったものであり、これは潜在的型付け（latent typing）とも呼ばれる。この仕組みは動的型付け（dynamic typing）の原点であり、実行時の逐次パターン判別はダックタイピングの源流にもなった。ML系を境にしてパターンを事前形成する静的型付け（static typing）が主流になった。その実装の代数的データ型は多項な型構築子の組み合わせであり、パラメトリック多相でジェネリック化された。Hindley–Milner型体系はこのパラメトリック多相に対応した型推論機能を提供した。関数型では強い型付け（strong typing）が主流であるが、ユニオン型（等価性による非交和型）による値の扱いは弱い型付け（weak typing）相当と見なせる。

型は、それを量化したターム（型付け値）を普通に扱える全称量（for all）のパターンと、そのタームの扱いに制限がある存在量（exists）のパターンに分かれる。全称量のパターンはプロパータイプ（proper type）と呼ばれる。プロパータイプは1個以上のタイプ（type）から形成される。タイプはプリミティブまたはコンポジットの総称である。型構築子はプロパータイプを構成するタイプを決めて同時にそのプロパータイプの識別子になる。プロパータイプはそれらタイプに依存（dependent）しているとされその依存関係の表現は、例えばタイプAとタイプBからなるプロパータイプCでは「A→B→C」のように表される。プロパータイプ内の1個以上のタイプが抽象化されると存在量のパターンになる。タイプの抽象化とは、型構築子内の要素を型変数にするジェネリック化と同義でありこれはパラトメトリック多相と言われる。存在量のパターンのタームは、抽象部分を残している型付け値になるのでその取扱いには様々な制限がかかる。これを全称量のパターンであるプロパータイプにするには、その型構築子への型引数の指定が必要になる。全称量のパターンであるプロパータイプと、そうでない存在量のパターンを区別する仕組みが型理論のカインドである。カインドではタイプは＊という総称記号になる。プロパータイプは「＊」と表現される。型引数を1個必要とするものは「＊→＊」になる。2個必要なら「＊→＊→＊」になり、これに型引数が1つ適用されると「＊→＊」になる。また、タイプに依存してプロパータイプを導出する仕組みが型構築子と呼ばれるのに対し、タームに依存してプロパータイプを導出する仕組みの方は型理論の依存型と呼ばれる。依存型の導出は、依存値×写像の直積で表現される。写像は依存関数とも呼ばれる。依存関数から導出される「型」も全称量のパターンと存在量のパターンに分かれており、依存型ではそれらが部分的に量化されていることもある。部分的に量化されている型とは、未確定の変数部分＝量化されていない部分を内包しているネーム存在と同義になる。この型としてのネーム存在は任意に簡約されてより柔軟なパターンマッチングを可能にする。型としてのネーム存在は量化されるとタームとしての値存在になり、それをまた依存値にした別の型の導出も可能である。依存型は型構築子をメインにするそれとは異なる型システムの下で実装されている。

多態性三種の三番目であるサブタイプ多相は、構造的サブタイピング（structural subtyping）と振る舞いサブタイピング（behavioral subtyping）に分かれている。構造的サブタイピングは前述の構造的型付けを汎化と特化の多相に応用したものであり、参照透過性の節で述べた派生構造型はその一つのパターン化である。またモナドも広義の構造的サブタイピングである。振る舞いサブタイピングの方は、データの操作的意味論の多相を扱うことから関数型とは相容れない部分が多い。関数型の代数的データ型とオブジェクト指向の抽象データ型は対象的なデータストラクチャと見なされている。前者がデータを主にしたデータ構造であるのに対して、後者は操作的意味論を主にしたデータ構造である。しかしオブジェクト指向との連携が模索される中で数々の手法も提示されている。動的型付けメインのLISP系ではS式の代わりに、各スロットに任意の変数を動的バインディングできるフレームレコードを用いる。その動的バインディング用レコードを1個以上引数にできる関数によって多重ディスパッチが表現される。動的バインディング用レコードの型チェックはダックタイピングで行われる。静的型付けメインのML系では、ジェネリッククラス（パラメトリック多相である総称的抽象データ型）の型変数のバリアンス（variance）を用いる。バリアンスとは型変数の派生関係を有効にして、型変数に適用できるクラスの幅を持たせることを指す。型変数のバリアンスには共変性（covariance）と反変性（contravariance）がある。共変性の型変数には適用クラスとその派生クラスを当てはめることができる。それに対して反変性の型変数には適用クラスとその基底クラスを当てはめることができる。反変性の用途はやや想像しにくいが、特化させた実装データに対するデータ抽象の汎化などに用いられる。また、関数の写像において基底クラスの引数→派生クラスの返り値は共変性、派生クラスの引数→基底クラスの返り値は反変性となる。バリアンスは境界的定量化（bounded quantification）の手法でも行われる。これは型引数または型変数を、共変ないし反変の基準とする注釈クラスで記号修飾するものである。共変である上限境界は、クラスのコンストラクタ（総称的抽象データ型の型構築子）の型引数を注釈クラスの派生クラスの適用に限定できる。反変である下限境界は、クラス内の型変数を注釈クラスの基底クラス範囲に差し戻せる。

歴史

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」といった派生言語が後年に登場している。また後年の「FP」にも影響を与えている。続く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年、BNF記法とFORTRAN開発の功績でこの年のチューリング賞を受けた計算機科学者ジョン・バッカスは「Can Programming Be Liberated From the von Neumann Style? -A Functional Style and Its Algebra of Programs-」と題した記念講演を行い、一説にはこれを境にして関数型（functional）というパラダイム名が定着したと言われている。なお同時に発表された「FP」は関数水準（function-level）言語として紹介されている。ノイマン型からの脱却を題目に掲げたバッカスは、FPのプログラムをアトム+関数+フォーム（=高階関数）の階層構造と定義し、代数を用いるフォームの結合で構築されると提唱した。

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」が初リリースされた。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年）←　APL

関数水準言語、動的型付け、先行評価

Standard ML　（1983年）←　ML、Hope、PASCAL

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

Caml　（1985年）←　ML

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

Miranda　（1985年）←　ML、Hope、SASL

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

Erlang　（1986年）←　LISP、Prolog、Smalltalk

動的型付け、先行評価

Clean　（1987年）←　Miranda

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

Haskell　（1990年）←　Scheme、Standard ML、Miranda、FP

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

Dylan　（1993年）←　Scheme、CLOS、ALGOL

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

R　（1993年）←　Scheme、CLOS

動的型付け、先行評価

Racket　（1995年）←　Scheme、Eiffel

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

OCaml　（1996年）←　Caml、Standard ML、Modula-3

ML派生、静的型付け、先行評価、オブジェクト指向

Scala　（2003年）←　Scheme、Standard ML、Haskell、Erlang、Smalltalk、Java

静的型付け、先行評価、オブジェクト指向

F#　（2005年）←　Standard ML、Haskell、Erlang、Scala、Python、C♯

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

Clojure　（2007年）←　Scheme、Haskell、Erlang、Java

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

Rust　（2010年）←　Scheme、Standard ML、Haskell、Erlang、C♯

静的型付け、先行評価

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

アルゴリズムのHello Worldと言えるフィボナッチ数を求めるプログラムは、チュートリアルなどでよく引き合いに出されるものであり、本稿でも手続き型言語との比較を兼ねて取り上げる。一般的な手続き型言語によるソースコードは以下のようになる。

FUNCTION fibona (num: INTEGER): INTEGER;
VAR
  x, y, tmp: INTEGER;
BEGIN
  x := 1;
  y := 1;
  FOR i := 2 TO num DO
  BEGIN
    tmp := x;
    x := y;
    y := y + tmp;
  END;    
  fibona := y;
END;

それに対して一般的な関数型言語によるソースコードは以下のようになる。

let rec fibona num = if num < 2 then 1 else fibona (num-2) + fibona (num-1)

コード行の羅列であるテキスト的な手続き型プログラミングと比較すると関数型プログラミングの方は、ガードとリミットによる分岐終点ルールで枠組みされたリーフ値と再帰関数のノードによるツリー化手順が一目で把握可能であり、ソースコードから式のツリー構造が直感的に浮かび上がってくる。同様のアルゴリズムで後続値とのペア（2-tuple）を表示するものは以下のようになる。

let rec fibona num =
  if num = 0 then (1, 1) else let (x, y) = fibona (num-1) in (y, x+y)
in
  fibona 5

result is (5, 8)

外部リンク

• なぜ関数プログラミングは重要か
• The Functional Programming Language XSLT - A proof through examples