「関数型プログラミング」の版間の差分
削除された内容 追加された内容
29行目:
関数型プログラムの基本文は[[式 (プログラミング)|式]]（''expression''）である。式は個体（''individual''）である値（''value''）と写像（''mapping''）である関数（''function''）の二つから構成される。関数の定義には[[演算子]]（''operator''）も含まれている。値は[[基本データ型]]（プリミティブ）と{{仮リンク|複合データ型（コンポジット）|en|Composite data type|label=}}および[[ラムダ計算]]で言われる変数（''variable''）を意味する。変数は[[束縛変数]]と[[自由変数と束縛変数|自由変数]]を指す。評価（''evaluation''）される前の式は、ラムダ計算で言われるネーム（''name''）と同義になる。ネームは数学上の数式または代数式に相当するものである。式内の変数部分が確定される前の式はラムダ抽象（''abstraction''）と同義になる。式内の変数部分を確定するのはラムダ適用（''application''）と同義になる。この式＝ネームが評価されると値になり、これはラムダ計算で言われる簡約（''reduction''）と同義になる。式は値と同一視されるのですなわち式と値は相互再帰の関係にある。式内の値は他の式の評価値である事があり、その式内にもまた他の値があるといった具合である。この解釈は[[高階論理|高階述語論理]]''と呼ばれる。高階述語論理＝[[高階関数]]の解釈下で引数または返り値として扱われる関数は[[第一級関数]]と呼ばれる。''
関数型プログラミングの関数は’’関数の型’’（''function type''）で分類される[[存在量化子|存在量]]の値である。プログラム的には式に引数を結び付ける機能であり、これは関数を引数に[[写像|適用]]する（''applying a function to an argument''）とされる。関数の式内の仮引数（''parameter''）箇所に渡された実引数（''argument''）が[[パターンマッチング]]手法で当てはめられ、先行（その時）または遅延（その後）タイミングで評価されて結果値が導出される。この仮引数箇所は束縛変数と呼ばれる。関数呼び出し時とは異なるタイミングで内容が決定される変数箇所は自由変数と呼ばれる。letとwhereで特定の式に向けて定義される変数は
’’関数の型’’は「第1引数の型→第x引数の型→評価値の型」というように形式化されておりこれはカリー化（''currying''）と呼ばれる。例として関数funcの型を<code>func::A→B→C</code>とするとこの場合、A型値に適用されたfuncは<code>B→C</code>という’’関数の型の値’’を返す事になり、それをB型値に適用するとC型の評価値が返る事になる。左からの引数にひとつひとつ適用する形にして、<code>B→C</code>のような中間的な’’関数の型の値’’が導出されるようにする仕組みが関数の[[カリー化]]である。カリー化は写像の[[量化]]（''quantify''）を扱う[[二階述語論理]]の実装である。カリー化によって関数funcの型は<code>func::A→(B→C)</code>と読み替えられるようになり、この場合にAにのみ適用して<code>B→C</code>という’’関数の型の値’’のまま保留することは部分適用（''partial application''）と呼ばれる。またカリー化による重要概念に関数合成（''function composition''）がある。これは合成演算子<code>.</code>（専用の二項演算子）を関数<code>f::B→C</code>に適用すると<code>(＊→B)→(＊→C)</code>が導出され、それを関数<code>g::A→B</code>に適用すると<code>(A→B)→(A→C)</code>となり関数<code>f . g::A→C</code>が導出されるというものである。合成演算子の左側の[[定義域]]と右側の[[値域]]が同じ型の場合のみ合成できる。高階関数的な連結である<code>f (g A)</code>と働きかた的には同じであるが、[[パイプライン処理]]の方に該当する関数連結（関数チェーン）と、カリー化に則った関数合成は異なる概念である。カリー化による部分適用や合成演算子から導出された’’関数の型の値’’を任意の変数に束縛して扱うのはポイントフリースタイル（''point-free style''）と呼ばれる。ポイントフリースタイルの変数を値に適用すると、他の値が返されるか又は他の’’関数の型の値’’が返される事になる。引数を部分適用された演算子はセクションと呼ばれてポイントフリースタイルでよく用いられる。[[カリー化]]準拠の’’関数の型’’は[[型理論]]の指数型（''quotient type''）に分類されるものである。
64行目:
静的型付けにおける[[データ構造|データストラクチャ]]のパターン（型）はコンパイル前ないし実行前に全て事前形成される。その実装例である[[代数的データ型]]はデータ構築子の組み合わせでパターンを構築し、パラメトリック多相に基づいて[[ジェネリックプログラミング|総称化]]したパターン内の要素＝型変数を、型構築子への型引数の組み合わせで特定した。''Hindley–Milner''型体系はこのパラメトリック多相に対応した[[型推論]]機能を提供している。型構築子（''type constructor''）は必要とする型引数の個数によって分類され、これは[[カインド (型理論)|カインド]]（''kind''）と呼ばれる。カインドは総称記号である<code>＊</code>の写像で型構築子の型種を表現する。型引数を必要としない型構築子と必要な型引数を全て付与された型構築子はプロパータイプと呼ばれ<code>＊</code>と表現される。プロパータイプは[[全称量化子|全称量]]の型である。型引数を1個必要とするものは<code>＊→＊</code>になり、2個必要なら<code>＊→＊→＊</code>になる。これらは[[存在量化子|存在量]]の型になる。<code>＊→＊→＊</code>に型引数が1つ付与されると<code>＊→＊</code>になり更に1つ付与すると<code>＊</code>のプロパータイプになる。全称量の型付け値（ターム）は普通に扱えるが、存在量の型付け値はその一部分が抽象化（大抵は環境依存値と同義）されたままの特別な値と見なされて一定の制限下で扱われる。
推論的型付け下の関数の扱いでは、人為的表記による意味づけを重視した記名的型付け（''nominal typing''）が取り入れられており、これで推論的型付けの枠組み内での[[多重定義|関数オーバーロード]]が表現されている。ここでの人為的表記による意味づけとは、型構築子/データ構築子/’’関数の型’’それぞれのパターン内の型変数に、[[型理論]]で言われる文脈（''context''）を付加することを指している。文脈の付加は制約（''constraint''）と呼ばれる。文脈の付加はアドホック多相と考えられており、代表的な実装例はそれと[[ジェネリックプログラミング]]を組み合わせた[[型クラス]]である。型クラスは、引数/計算値/評価値などを[[総称型]]化したジェネリック関数群の’’関数の型’’と式内容を定義できる機能であり、同時に推論的型付けと共存する関数オーバーロードの実装と、特定の意味づけ型を扱うための関数モジュールを定義するための手段になっている。型クラスの定義構文では上述のジェネリック関数群が定義され、その型クラス名が文脈記号になる。型構築子の定義に文脈を付加すると、その型クラスのジェネリック関数群にその型構築子＝型を当てはめた関数群がコンパイル時に自動生成される（deriving）。また文脈を付加して当てはめ関数群を自動生成（instance）した上で、その型構築子＝型のための当てはめ関数
'''動的型付け'''
86行目:
モナド値は付加モナドと自由モナド（Maybe/例外/有限リストモナドなど）以外では、実質的に存在量の値になるので普通の値のように扱うことは出来ない。ただし付加/自由モナドでも参照透過性を維持するためには存在量と同等に扱う必要が出てくる。<code>return</code>を基本値に適用してモナド値を表現することからモナド処理は始まる。基本値とは扱うモナドに合わせた任意の値である。そのモナド値は圏としてのユニークIDを持つことになる。ここで基本値を<code>A</code>としそのモナド値を<code>MA</code>とする。<code>MA</code>にbindを適用して<code>(A→MB)→MB</code>という写像を導出する。その写像は先の<code>MA</code>と同じ圏IDを備えたものになる。その写像をモナド関数<code>(A→MB)</code>に適用すると、そのモナド関数内では渡された<code>A</code>やその他の値などに<code>return</code>を適用して表現されるモナド値の圏IDは<code>MA</code>のもので共通化される。モナド関数内においての<code>return</code>は基本値をモナド値に代入する機能と見てよい。<code>return</code>は用途別関数にそれぞれラッピングされて使われるのが普通である。空引数からモナド値を表現する<code>return</code>もありこれはモナドプリミティブ（''monadic primitive''）と呼ばれ、この場合はモナド値の圏IDが暗黙引数になっている。モナド値はファイルハンドルのようなものと考えると分かりやすくなり、モナド値を直接引数にできる専用関数も存在する。モナド関数内ではモナド値から基本値を取り出す演算子が有効になる。それは<code>A←MA</code>のように表現されてコモナド（''comonad''）と呼ばれる機能になる。抽出した基本値からの処理の中で再度<code>return</code>が行われる。モナド関数は自己関手内容に見立てられているので、その中では<code>return</code>の繰り返しによる事実上の再代入処理が許されている。その論理的な辻褄合わせの要点になる<code>bind</code>の正当性および計算可能性を表現するためにファンクタ則とモナド則の等式がプログラム内で定義されている。ここでいわゆる圏論の知識が必要になるがその説明は先送りする。モナド関数はモナド値を返しそれに再度<code>bind</code>を適用できるのでこれがモノイドを意味している。モナド関数の外での<code>return</code>は毎時ユニークな圏IDのモナド値を表現するので同じ基本値でもその都度異なる圏が表現される事になり、これが[[自然変換]]（[[関手圏]]の[[射 (圏論)|射]]）演算子の呼称由来になっている。
モナドは'''ファンクタ'''（''functor''）の派生文脈にされることが多いが、これは<code>bind</code>を形成するクライスリ射と<code>join</code>の合成の持ち上げ（関手）に<code>fmap</code>が使われるからである。ファンクタ文脈は関
== 歴史 ==
| |||