긍정적 인 양의 양화 기호를 외부로 들어 올리는 것은 유효한가요?

Question

이 질문은 #haskell에 대한 토론에서 나왔습니다.

깊이 중첩 된 포알을 맨 위로 올리는 것이 항상 올바른지?

예 :

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

우리가 일반적으로 그냥 (P(a) -> S) -> T

내가 아는 작성합니다

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

(에 (P, S, T는 metavariables로 이해 될 수있는 곳) 마지막으로 ->의 오른쪽과 같은 몇 가지 긍정적 인 위치에서 볼거리를 수집 할 수 있습니다.

이것은 고전 논리에서 유효하므로 불합리한 생각은 아니지만 일반적으로 직관 론에서는 유효하지 않습니다. 그러나 각 형식 변수가 "호출자가 선택"하거나 "호출 수신자가 선택한"한정 기호에 대한 나의 비공식적 인 게임 이론 직관은 실제로 두 가지 선택 만 가능하며 "호출자가 선택한"옵션을 모두 끌어 올 수 있음을 나타냅니다. 상단. 게임에서 움직임의 인터리브가 중요하지 않으면?

Answer 1

는

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

을 가정하고이 논의 S = (P Int, P Char)을 위해 수 있습니다. 가능한 타입 올바른 호출은 다음과 같을 수 S은 위와입니다

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

지금,

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

을 가정합니다. 이제는 bar을 호출하기가 어렵습니다! 의는 a = Int에 전화를 해 봅시다 :

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

이제 우리는 단순히 x에서 파생 할 수없는 something :: P Char이 필요합니다. a = Char 인 경우에도 마찬가지입니다. a이 Int, Char이 아닌 경우 더 악화됩니다.

당신은 직관 론을 언급했습니다. 이 로직에서 foo의 유형이 bar보다 강하다고 볼 수 있습니다. 더 강력한 가설로서, foo 유형은 증명에서 더 많은 경우에 적용될 수 있습니다. 따라서 용어로는 foo이 더 많은 상황에서 적용 가능하다는 것을 발견하는 것은 놀라운 일이 아닙니다. :)