パラメトリシティ

プログラミング言語理論において、パラメトリシティは、パラメトリック多態関数が持つ抽象的な均一性特性であり、多態関数のすべてのインスタンスが同じように動作するという直感を捉えています。

集合Xと、 Xからそれ自身への関数の型T ( X ) = [ X → X ] に基づくこの例について考えてみましょう。twice _X ( f ) = f ∘ fによって与えられる高階関数twice _X  : T ( X ) → T ( X ) は、集合Xから直感的に独立しています。集合Xによってパラメーター化されたこのようなすべての関数twice _Xの族は、「パラメーター的に多態的な関数」と呼ばれます。これらの関数の族全体を単にtwice と書き、その型をX . T ( X ) → T ( X ) と書きます。個々の関数twice _{X は}、多態的な関数のコンポーネントまたはインスタンスと呼ばれます。すべてのコンポーネント関数twice _{X は}同じ規則によって与えられるため、「同じように」動作することに注意してください。各T ( X ) → T ( X )から任意の関数を 1 つ選択することによって得られる他の関数族には、このような統一性はありません。これらは「アドホック多態的な関数」と呼ばれます。 パラメトリシティは、 twiceなどの均一に作用する族が持つ抽象的な特性であり、アドホック族と区別するものである。パラメトリシティを適切に形式化すれば、型X . T ( X ) → T ( X ) のパラメトリック多相関数が自然数と 1 対 1 であることを証明することができる。自然数nに対応する関数は、規則f f ⁿ、すなわちnの多相チャーチ数によって与えられる。対照的に、すべてのアドホック族のコレクションは、集合としては大きすぎるであろう。 ${\displaystyle \forall}$${\displaystyle \forall}$ ${\displaystyle \mapsto}$

パラメトリシティ定理はもともとジョン・C・レイノルズによって提唱され、抽象定理と呼ばれていました。^[1]フィリップ・ワドラーは論文「無料の定理！」^{[2]で、パラメトリシティを応用して、} パラメトリック多型関数に関する定理をその型に基づいて 導き出す方法について説明しました。

パラメトリシティは、 Haskell プログラミング言語のコンパイラに実装されている多くのプログラム変換の基礎です。これらの変換は、Haskell の非厳密なセマンティクスのため、Haskell では従来正しいと考えられていました。Haskellは遅延プログラミング言語であるにもかかわらず、演算子などの特定の基本操作をサポートしています。これにより、いわゆる「選択的厳密性」が可能になり、プログラマが特定の式の評価を強制できるようになります。Patricia Johann と Janis Voigtlaender は、論文「seqがある場合の自由な定理」^[3]で、これらの操作があるため、一般的なパラメトリシティ定理は Haskell プログラムには当てはまらないことを示し、したがって、これらの変換は一般に不健全です。 seq

• パラメトリック多態性
• 非厳密なプログラミング言語

• ワドラー：パラメトリシティ