11

この質問は #haskell の議論で出てきました。

深くネストされた forall の発生が正の場合、その forall を一番上に持ち上げることは常に正しいですか?

例えば：

((forall a. P(a)) -> S) -> T

(ここで、P、S、T はメタ変数として理解されるべきです)

forall a. (P(a) -> S) -> T

(通常は次のように記述します。(P(a) -> S) -> T

ラストの右側など、いくつかのポジティブな位置からフォーラルを収集することが確かに許可されていることを私は知っています->。

これは古典論理では有効なので、ばかげた考えではありませんが、一般的に直観主義論理では無効です。ただし、各型変数が「呼び出し元によって選択された」または「呼び出し先によって選択された」という量指定子の非公式のゲーム理論の直感は、実際には2つの選択肢しかなく、すべての「呼び出し元によって選択された」オプションを持ち上げることができることを示唆していますトップ。ゲーム内の動きのインターリーブが重要でない限り?

4

1 に答える 1

3

推定

foo :: ((forall a. P a) -> S) -> T

と、この議論のためにしましょうS = (P Int, P Char)。考えられる型の正しい呼び出しは次のようになります。

foo (\x :: (forall a. P a) -> (x,x))

さて、仮定します

bar :: forall a. (P a -> S) -> T

場所Sは上記の通り。発動しにくくなりましたbar！で呼び出してみましょうa = Int:

bar (\x :: P Int -> (x, something))

ここで、something :: P Charから単純に導出できない が必要xです。の場合も同様ですa = Char。aが 以外の場合はInt, Char、さらに悪化します。

あなたは直観主義の論理について言及しました。そのロジックでは、 のタイプが のタイプfooよりも強力であることがわかるかもしれませんbar。したがって、より強力な仮説として、 の型はfoo証明のより多くのケースに適用できます。fooしたがって、用語として、より多くの文脈で適用できることがわかっても驚くべきことではありません! :)

于 2014-02-28T18:44:12.107 に答える