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

関数型プログラミングは[[数理論理学]]と代数系をルーツにし、[[ラムダ計算]]と[[コンビネータ論理]]を幹にして構築され、[[LISP]]言語が実装面の先駆になっている。応用面では[[圏論]]がパラダイムモデルにされている。関数の数学的な純粋性を指向したものは純粋関数型言語と個別に定義されている。[[命令型プログラミング]]言語では単に有用な構文スタイルとして扱われている事が多い。[[高階関数]]、[[第一級関数]]、{{仮リンク|関数合成|en|Function composition (computer science)|label=}}、{{仮リンク|部分適用|en|Partial application|label=}}、[[無名関数]]、[[クロージャ]]、[[継続]]、[[ボトム型|部分関数]]、{{仮リンク|ポイントフリー|en|Tacit programming|label=}}、[[パイプライン処理|パイプライン]]、[[イテレータ]]、[[ジェネレータ (プログラミング)|ジェネレータ]]、[[代数的データ型]]、[[型推論]]、[[パターンマッチング]]、[[ガード (プログラミング)|ガード]]、{{仮リンク|パラメトリック多相|en|Parametric polymorphism|label=}}、{{仮リンク|アドホック多相|en|Ad hoc polymorphism|label=}}、[[末尾再帰]]、[[束縛変数]]、[[イミュータブル]]、{{仮リンク|純粋関数|en|Pure function|label=}}などが{{誰範囲|date=2020年5月|関数型プログラミングのスタイル要素として挙げられる}}。

*[[無名関数]]は引数をピュア[[写像|マッピング]]する純粋関数であるが、毎回違う値が渡される用途から事実上[[メモ化]]できない事がコーディング上の利便性を除いた存在理由になっている。[[クロージャ]]の引数[[写像|マッピング]]は式内の自由変数に影響され、またその自由変数に作用する事もある即ちという副作用要素を閉包した非純粋関数である。

*イミュータブル性が重視されない場合、関数の終端式での再帰は、実引数の更新＋先端式へのアドレスジャンプと同等に見なせるので専らそちらに最適化される。これは[[末尾再帰]]と呼ばれる。同様の仕組みで相互再帰を同様に最適化したものは兄弟再帰（''sibling recursion''）と呼ばれもある。

*部分関数は引数によって[[ボトム型]]を返せになる関数である。ボトム型は命令型言語に虚（''falsity''）と見なされておける例外発生と同等り、式のツリーないし写像の連鎖の失敗した終着点に解釈できなる。

*左辺のもので右辺のものを置き換えられるという代数的データ型間の[[項書き換え]]ルール代用（''substitution''）規則を定義できる。これは型シノニムと呼ばれる。これは厳密には異なるが[[継承 (プログラミング)|継承]]の[[リスコフの置換原則]]に似たものであをイメージすると分かりやすい。

*直積型は、(A, B) のような[[タプル]]のパターンを表わす。または標準的な[[構造体|レコード]]のパターンを表現わする。

*非交和型は、(A | B) のような[[共用体|修飾共用体]]または[[列挙型]]のパターンを表わす。前者は型推論による等価性で、後者は評価による等値性で識別される非交和である。前者はユニオン型（''union type''）と個別定義されてもいる。

関数型プログラミングにおける[[評価戦略]]とは「式存在」を「値存在」にする評価タイミングの定義を指す。これはまず正格評価（''strict evaluation''）と非正格評価（''non-strict evaluation''）の二つに大別される。前者正格評価の式存在は、関数による適用と同時に評価されて値存在になり、または変数による束縛と同時に評価されて値存在になる。関数の引数節で直積された式存在は理論上全て同時に評価される事になる。その実装は直積された式存在を副作用を伴わずに並行計算するか、そうでない場合は一つ一つ評価していく事になる。単に一つ一つ評価していくものは[[先行評価]]になり、ここでも副作用を伴わない事が原則とされるが必須ではなくなる。

後者の非正格評価はほとんどのケースで[[遅延評価]]と同義の言葉になる。遅延評価の式存在は、関数に適用されても式存在のままであり、または変数に束縛されても式存在のままである。後続式において改めて他の関数ないし演算子に適用される時に初めて評価されて値存在になり、または改めて他の変数に束縛される時に初めて評価されて値存在になる。これが遅延評価のデフォルトタイミングである。が、[[継続]]コール（''call/cc''）手法や不可反駁（''irrefutable''）指定によって更に評価を遅延させる事もできる。継続コールは変数束縛した第一級関数またはクロージャを任意のタイミングで評価して値を導出できる機能である。これは値の導出後も式存在のままなので再利用できる。コール前の部分適用とコール時の引数適用、クロージャの方では自由変数への任意時代入も可能である。不可反駁指定はその式存在の変数部分が不特定で[[ボトム型]]を導出する場合は評価を取り止め、特定してる場合のみに評価を成立させて値存在にする機能である。ただしこれは遅延パターンマッチングでワンクッション置くため等価性審査から評価値写像につなげる為の内包表記用途にほぼ限定されている。また代数的データ型の式パターンの多くは全て遅延評価対象になであり、これによって[[共用体]]、無限リスト、[[再帰データ型]]の表現が可能になっている。

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

[[参照透過性]]とは関数は同じ引数値に対して必ず同じ評価値を恒久的に導出し、その評価過程において現行計算枠外の情報資源に一切の作用を及ぼさないというプロセス上の枠組みを意味する。現行計算枠外のいずれかの情報資源が変化するのと同時にいずれかの関数の評価過程も変化してしまう現象は[[副作用 (プログラム)|副作用]]と呼ばれる。参照透過性はこの副作用の排除も同時に意味している。参照透過性のに則した関数実装は関数の純粋化と呼ばれる。参照透過性は関数の純粋化の他、変数の再代入をプログラムから代入（＝排除する事で成立する。それによってあらゆる値の写像の履歴がプログラム開始時に宣言（''assignmentdeclarative''）された初期値まで遡れるようになる。この膨大な写像の履歴ツリーの解析と模型化は[[プロセス計算|プロセス微積分]]ないし[[プロセス代数]]と呼ばれ、≠並行プログラミングの支柱にされている。並行プログラミングの基本メカニズムは、全プロセスをまず無制約に並行実行させておき、どこかで不整合（''substitutionconflict''）処理が発生した場合は一定の関連プロセスを排除整合性が取れる履歴ツリー上の写像位置まで巻き戻すというものである事。過去に戻ったプロセスは不整合が反映された別の写像ルートを辿ることになるが、そのルート変化は未来情報の反映になるので具体的副作用に成立すは当たらない。この時に履歴ツリーが用いられる。従って写像履歴の改ざんにつながる再代入は厳禁になり、ある時点の写像をただ書き留めておく[[束縛変数]]と、旧値の更新を新値の産出で代替した[[イミュータブル]]が不可欠になる。ループは再帰で行われ、条件分岐は[[代数的データ型]]の[[依存型]]で表現される。

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