F-オメガ用語

Question

を理解することができません私はF _ωに関する論文を読んでいて、この文の背後にある理由を理解することはできません：FORALL

種類のタイプ項（＆; γ：* F γ。 → β）は、Fが常にβを返す定数関数であることを示しています。

私は 'γ → β F' を推測するタイプの用語、すなわち、矢印タイプです。この矢印タイプは、タイプアプリケーション 'F γ'によって計算されたタイプの引数を取り、タイプβの値を返す関数のタイプです。

これが当てはまる場合、Fはいつも常にβを返す定数（型）関数ですか？ αを返し、型チェッカーを満たしている任意の型の関数ではありませんか？

お時間をいただきありがとうございます。

Answer 1

私自身の質問に答える。

私はその理由がparametricityだと思います。

「F γ」は例えばαために、任意の型を返すことができた場合、（そのタイプ＆FORALLによって搬送され、タイプ）関数はα → βのタイプを有するであろう。

Parametricityしたがって、「F γ」は常にβを返すことを意味し、タイプβ → βで、即ち、この多型関数のすべてのインスタンスは、それが恒等関数である場合にのみ可能である同じ挙動を有するべきであることを指示します。