14

idは type の唯一の関数であり、 typea -> aの fst唯一の関数です(a,b) -> a。これらの単純なケースでは、これは非常に簡単にわかります。しかし、一般的に、これをどのように証明しますか? 同じタイプの可能な関数が複数ある場合はどうなりますか?

あるいは、関数の型が与えられた場合、その型の一意の (これが真である場合) 関数をどのように導出しますか?

編集:型に制約を追加し始めたときに何が起こるかに特に興味があります。

4

1 に答える 1

15

あなたが探している結果は、レイノルズのパラメトリック性から導き出されたものであり、ワドラーが無料の定理で最も有名に示したものです。

私が見た基本的なパラメトリック性の結果を証明する最もエレガントな方法は、「シングルトン型」の概念を使用しています。基本的に、ADT が与えられた場合

data Nat = Zero | Succ Nat

索引付けされたファミリー (GADT とも呼ばれます) が存在します。

data SNat n where
   SZero :: SNat Zero
   SSucc :: SNat n -> SNat (Succ n)

そして、すべての型を型付けされていない言語に「消去」し、同じものに消去することNatにより、言語にセマンティクスを与えることができます。SNat次に、言語の入力規則によって

id (x :: SNat n) :: SNat n

SNat nセマンティクスは消去によって与えられるため、関数は引数の型を使用できないため、idいずれかから返される唯一の値Natは、与えられた数値です。この基本的な議論はパラメトリック性の結果のほとんどを証明するために拡張することができ、Karl Crary によってA Simple Proof Technique for Parametricity Resultsで使用されましたが、ここでのプレゼンテーションはStone と Harperに触発されたものです

于 2012-11-27T06:05:50.467 に答える