パラメトリック多型

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

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

パラメトリック多相性を研究するための一般的な理論的手法はシステムFであり、これは単純な型付きラムダ計算を型に対する量化で拡張したものである。

引数の型に依存しない関数を記述することは可能です。例えば、恒等関数などが挙げられます。${\displaystyle {\mathsf {id}}(x)=x}$引数をそのまま返します。これにより、次のような潜在的な型のファミリーが自然に生まれます。${\displaystyle {\mathsf {Int}}\to {\mathsf {Int}}}$、$\displaystyle {\mathsf {Bool}}\to {\mathsf {Bool}}$、${\displaystyle {\mathsf {String}}\to {\mathsf {String}}}$など。パラメトリック多相性により${\displaystyle {\mathsf {id}}}$全称量化型変数を導入することにより、単一の最も一般的な型を与える：

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

多相定義は、任意の具体的な型を代入することでインスタンス化できます。${\displaystyle \alpha }$これにより、潜在的な型の全ファミリーが得られます。^{[ 3 ]}

恒等関数は特に極端な例ですが、他の多くの関数もパラメトリック多相性の恩恵を受けています。たとえば、${\displaystyle {\mathsf {append}}}$2 つのリストを連結する関数は、リストの要素を検査せず、リストの構造自体のみを検査します。したがって、${\displaystyle {\mathsf {append}}}$類似の型ファミリーを与えることができます。${\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 ]}$

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

パラメトリック多相関数${\displaystyle {\mathsf {id}}}$そして${\displaystyle {\mathsf {append}}}$任意の型でパラメータ化されていると言われている${\displaystyle \alpha }$[ ^{4 ]}両方^​${\displaystyle {\mathsf {id}}}$そして${\displaystyle {\mathsf {append}}}$は単一の型でパラメータ化されますが、関数は任意の数の型でパラメータ化できます。たとえば、${\displaystyle {\mathsf {fst}}}$そして${\displaystyle {\mathsf {snd}}}$ペアの最初の要素と2番目の要素をそれぞれ返す関数には、以下の型を指定できます。

${\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 {Bool}}}$呼び出しの中で${\displaystyle {\mathsf {fst}}}$全体の式の型は${\displaystyle {\mathsf {Int}}}$。

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

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

1980年代、LeivantはGirardとReynoldsのシステムFの階層化（つまり述語的）バージョンを導入した。Leivantのアプローチは、関数コンストラクタ内のネスト深度を測定する量化子のランクの概念に基づいている。^{[ 7 ]}この観点から、MLアプローチはランク1多相性に限定される。Haskellは1990年代に高ランクのパラメトリック多相性を採用した。例えば、Haskellではランク2のパラメトリック多相性を使用してモナドを定義しておりrunST、これは「命令型プログラミングの分離された領域」を持つ型と効果のシステムを効果的にシミュレートしている。^{[ 8 ]}型レベルでは、状態の分離は基本的に、における状態に対するより深いランク2の量化から生じるrunST。（これだけでは、の実行時意味論を形式的に記述するには不十分であるrunST。後者については、分離論理などの追加の要素が必要となる。^{[ 9 ]}）

型は、そのルートから次の要素へのパスが存在しない場合、ランクk (固定整数kに対して) であると言われます。${\displaystyle \forall }$量指定子は、型が木として描かれている場合、k個以上の矢印の左側に渡されます。 ^{[ 1 ] : 359}型システムがランクk多相性をサポートするとは、ランクがk以下の型を許容する場合を指します。たとえば、ランク 2 多相性をサポートする型システムは、${\displaystyle (\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T}$しかしそうではない${\displaystyle ((\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T)\rightarrow T}$任意のランクの型を許容する型システムは、「ランクn多相的」であると言われる。

（このランクの概念は、古典論理における量化子ランクの定義とは異なります。なぜなら、ここでは非量化子結合子に対する入れ子の深さを測定するのに対し、古典論理では非量化子結合子はそれらの下にネストされた量化子のランクを増加させませんが、他の量化子は増加させるからです。）

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

• パラメトリック性
• 多相再帰
• 型クラス#高階多相性
• 特性（コンピュータプログラミング）

• 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 年)、「最高数学解釈と最高学力の解釈」 (博士論文) (フランス語)、パリ第 7 大学。
• Reynolds, John C. (1974)、「Towards a Theory of Type Structure」、Colloque Sur la Programmation、Lecture Notes in Computer Science、vol.  19、パリ、pp. 408–425、土井：10.1007/3-540-06859-7_148、ISBN  978-3-540-06859-4{{citation}}: CS1 maint: 場所の発行元が見つかりません (リンク)。
• Milner, Robin (1978). "プログラミングにおける型多相性の理論" (PDF) . Journal of Computer and System Sciences . 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 Press. ISBN 978-0-262-16209-8。