パラメトリック多態性

プログラミング言語と型理論では、パラメトリック多態性により、実際の型の代わりに変数を使用して単一のコードに「ジェネリック」型を与え、必要に応じて特定の型でインスタンス化することができます。^{[1] ：340}パラメトリック多態関数とデータ型は、それぞれジェネリック関数とジェネリックデータ型と呼ばれることもあり、ジェネリックプログラミングの基礎を形成します。

パラメトリック多態性は、アドホック多態性と対比されることがあります。パラメトリック多態性の定義は均一です。つまり、インスタンス化される型に関係なく、同じように動作します。^{[1] : 340  [2] : 37}対照的に、アドホック多態性の定義では、型ごとに異なる定義が与えられます。したがって、アドホック多態性では、型ごとに個別の実装を提供する必要があるため、通常、このような異なる型の限られた数しかサポートできません。

引数の型に依存しない関数を記述することも可能です。たとえば、恒等関数は 引数をそのまま返します。これにより、 、 、 などの潜在的な型のファミリーが自然に生じます。パラメトリック多態性により、普遍的に量化された型変数 を導入することで、に単一の最も一般的な型を与えることができます。 ${\displaystyle {\mathsf {id}}(x)=x}$${\displaystyle {\mathsf {Int}}\to {\mathsf {Int}}}$${\displaystyle {\mathsf {Bool}}\to {\mathsf {Bool}}}$${\displaystyle {\mathsf {文字列}}\to {\mathsf {文字列}}}$${\displaystyle {\mathsf {id}}}$

${\displaystyle {\mathsf {id}}:\forall \alpha .\alpha \to \alpha }$

多態的定義は、を任意の具体的な型に置き換えることによってインスタンス化することができ、潜在的な型の完全なファミリが生成されます。^[3]${\displaystyle \alpha}$

恒等関数は特に極端な例ですが、他の多くの関数もパラメトリック多態性の恩恵を受けています。たとえば、2つのリストを連結する関数は、リストの要素を検査せず、リスト構造自体のみを検査します。したがって、 には、、 などの同様の型ファミリを与えることができます。ここで、 は型 の要素のリストを表します。したがって、最も一般的な型は ${\displaystyle {\mathsf {追加}}}$${\displaystyle {\mathsf {追加}}}$${\displaystyle [{\mathsf {Int}}]\times [{\mathsf {Int}}]\to [{\mathsf {Int}}]}$${\displaystyle [{\mathsf {Bool}}]\times [{\mathsf {Bool}}]\to [{\mathsf {Bool}}]}$${\displaystyle [T]}$${\displaystyle T}$

${\displaystyle {\mathsf {append}}:\forall \alpha .[\alpha ]\times [\alpha ]\to [\alpha ]}$

ファミリ内の任意の型にインスタンス化できます。

やのようなパラメトリック多相関数は、任意の型に対してパラメータ化されていると言われます。^[4]と はどちらも単一の型に対してパラメータ化されていますが、関数は任意の数の型に対してパラメータ化できます。たとえば、ペアの最初の要素と 2 番目の要素をそれぞれ返す関数と関数には、次の型を指定できます。 ${\displaystyle {\mathsf {id}}}$${\displaystyle {\mathsf {追加}}}$${\displaystyle \alpha}$${\displaystyle {\mathsf {id}}}$${\displaystyle {\mathsf {追加}}}$${\displaystyle {\mathsf {fst}}}$${\displaystyle {\mathsf {snd}}}$

${\displaystyle {\begin{aligned}{\mathsf {fst}}&:\forall \alpha .\forall \beta .\alpha \times \beta \to \alpha \\{\mathsf {snd}}&:\forall \alpha .\forall \beta .\alpha \times \beta \to \beta \end{aligned}}}$

式 では、が にインスタンス化され、の呼び出しでが にインスタンス化されるため、式全体の型は になります。 ${\displaystyle {\mathsf {fst}}((3,{\mathsf {true}}))}$${\displaystyle \alpha}$${\displaystyle {\mathsf {Int}}}$${\displaystyle \beta}$${\displaystyle {\mathsf {ブール}}}$${\displaystyle {\mathsf {fst}}}$${\displaystyle {\mathsf {Int}}}$

パラメトリック多態性を導入するために使用される構文は、プログラミング言語によって大きく異なります。たとえば、Haskellなどの一部のプログラミング言語では、量指定子は暗黙的であり、省略できます。^[5]他の言語では、パラメトリック多態性関数の呼び出しサイトの一部またはすべてで型を明示的にインスタンス化する必要があります。 ${\displaystyle \forall \alpha }$

パラメトリック多態性は、1975年にMLで初めてプログラミング言語に導入されました。^[6]現在、Standard ML、OCaml、F#、Ada、Haskell、Mercury、Visual Prolog、Scala、Julia、Python、TypeScript、C++などに存在します。Java 、C#、Visual Basic .NET、Delphiはそれぞれ、パラメトリック多態性のための「ジェネリック」を導入しています。型多態性の実装の中には、表面的にはパラメトリック多態性に似ていますが、アドホックな側面も導入しているものがあります。1つの例として、C++のテンプレート特殊化があります。

述語型システム（冠頭多態システムとも呼ばれる）では、型変数は多態型でインスタンス化されない場合がある。^{[1] : 359–360}述語型理論には、Martin-Löf型理論とNuprlが含まれる。これは、「MLスタイル」または「Let多態性」と呼ばれるものと非常によく似ている（技術的には、MLのLet多態性には他にもいくつかの構文上の制約がある）。この制約により、多態型と非多態型の区別が非常に重要になる。そのため、述語システムでは、多態型は、モノタイプと呼ばれることもある通常の（モノモーフィックな）型と区別するために、型スキーマと呼ばれることがある。

述語性の結果、すべての型は、すべての量指定子を最も外側 (冠頭) の位置に配置する形式で記述できます。たとえば、上記の関数は次の型を持ちます。 ${\displaystyle {\mathsf {追加}}}$

${\displaystyle {\mathsf {append}}:\forall \alpha .[\alpha ]\times [\alpha ]\to [\alpha ]}$

この関数をリストのペアに適用するには、結果の関数の型が引数の型と一致するように、変数を具体的な型に置き換える必要があります。非述語的システムでは、は、それ自体が多態的な型を含む任意の型にすることができます。したがって、任意の型の要素を持つリストのペアに適用できます。それ自体のような多態的な関数のリストにも適用できます。言語 ML の多態性は述語的です。^[要出典]これは、述語性と他の制限により、型システムが十分に単純になり、完全な型推論が常に可能になるためです。 ${\displaystyle T}$${\displaystyle \alpha}$${\displaystyle T}$${\displaystyle {\mathsf {追加}}}$${\displaystyle {\mathsf {追加}}}$

実際の例として、OCaml ( MLの派生または方言) は型推論を実行し、非予測的多態性をサポートしますが、非予測的多態性が使用される場合、プログラマーが明示的な型注釈を提供しない限り、システムの型推論は不完全になることがあります。

一部の型システムでは、他の型コンストラクタが述語的であるにもかかわらず、非述語的な関数型コンストラクタをサポートしています。たとえば、高位ポリモーフィズムをサポートするシステムでは、その型が許可されますが、そうでない場合もあります。^[7]${\displaystyle (\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T}$${\displaystyle [\forall \alpha .\alpha \rightarrow \alpha ]}$

型をツリーとして描いたときに、ルートから量指定子へのパスがk個以上の矢印の左側を通過しない場合、その型はランクk (ある固定整数kに対して)であると言われます。 ^{[1] : 359}型システムがランクkポリモーフィズムをサポートすると言われているのは、ランクがk以下の型を許可する場合です。たとえば、ランク 2 ポリモーフィズムをサポートする型システムは、 を許可しますが、 は許可しません。任意のランクの型を許可する型システムは、「ランクnポリモーフィック」であると言われます。 ${\displaystyle \forall}$${\displaystyle (\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T}$${\displaystyle ((\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T)\rightarrow T}$

ランク2多態性に対する型推論は決定可能であるが、ランク3以上では決定不可能である。^{[8] [1] : 359}

非述語的多態性（ファーストクラス多態性とも呼ばれる）は、パラメトリック多態性の最も強力な形式です。^{[1] ：340}形式論理では、定義が自己参照的である場合に非述語的であると言われます。型理論では、これは型がそれに含まれる量指定子のドメイン内に存在する能力を指します。これにより、多態型を含む任意の型で任意の型変数をインスタンス化できます。完全な非述語性をサポートするシステムの例としては、System Fがあり、それ自体を含む任意の型で インスタンス化できます。${\displaystyle \forall \alpha .\alpha \to \alpha }$

型理論において、最も頻繁に研究される非述語型付きλ計算は、ラムダキューブ、特にシステム F の計算に基づいています。

1985 年、Luca CardelliとPeter Wegner は、型パラメータに制限を設けることの利点を認識しました。 ^[9]多くの操作はデータ型に関する知識を必要としますが、それ以外はパラメトリックに機能します。たとえば、項目がリストに含まれているかどうかを確認するには、項目が等しいかどうかを比較する必要があります。Standard MLでは、形式''aの型パラメータは等価演算が利用できるように制限されているため、関数の型は''a × ''a list → bool になり、''a は等価性が定義された型のみになります。Haskell では、型が型クラスに属することを要求することで制限が実現されるため、同じ関数は Haskell では型を持ちます。パラメトリック多態性をサポートするほとんどのオブジェクト指向プログラミング言語では、パラメータを特定の型のサブタイプに制約できます( 「サブタイプ多態性」および「ジェネリックプログラミング」の記事を参照)。 ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$

• パラメトリシティ
• 多態的再帰
• 型クラス#高次多態性
• 特性（コンピュータプログラミング）

• Hindley, J. Roger (1969)、「組み合わせ論理におけるオブジェクトの主要な型スキーム」、アメリカ数学会誌、146 : 29–60、doi :10.2307/1995158、JSTOR  1995158、MR  0253905。
• ジラール、ジャン＝イヴ(1971)。 「ゲーデルの分析の解釈の拡張、および分析とタイプの理論の分析の応用」。第 2 回スカンジナビア論理シンポジウムの議事録。論理学と数学の基礎の研究（フランス語）。 Vol. 63.アムステルダム。 63–92ページ。土井：10.1016/S0049-237X(08)70843-7。ISBN 9780720422597。
• ジラール、ジャン＝イヴ(1972)、Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur (博士論文) (フランス語)、パリ第 7 大学。
• Reynolds, John C. (1974)、「Towards a Theory of Type Structure」、Colloque Sur la Programmation、Computer Science の講義ノート、19 年、パリ: 408–425、doi :10.1007/3-540-06859-7_148、ISBN 978-3-540-06859-4。
• ミルナー、ロビン( 1978)。「プログラミングにおける型多態性の理論」(PDF)。コンピュータとシステム科学ジャーナル。17 ( 3): 348–375。doi :10.1016/0022-0000(78)90014-4。S2CID  388583。
• Cardelli , Luca ; Wegner, Peter (1985年12 月)。「型、データ抽象化、およびポリモーフィズムの理解について」( PDF)。ACM Computing Surveys。17 ( 4): 471–523。CiteSeerX 10.1.1.117.695。doi : 10.1145 /6041.6042。ISSN 0360-0300。S2CID  2921816  。 
• ピアス、ベンジャミン C. (2002)。型とプログラミング言語。MIT プレス。ISBN 978-0-262-16209-8。