하스켈 및 Rank-N 다형성

Question

가상의 하스켈 코드는 정확히 무엇이 틀렸습니까? 내 머리 속에서 컴파일하면 "1"이 출력됩니다.

foo :: forall a. forall b. forall c. (a -> b) -> c -> Integer -> b 
foo f x n = if n > 0 then f True else f x 

bar :: forall a. a -> Integer 
bar x = 1 

main = do 
    putStrLn (show (foo bar 1 2)) 

GHC는 불평 :

$ ghc -XRankNTypes -XScopedTypeVariables poly.hs 

poly.hs:2:28: 
    Couldn't match expected type `a' against inferred type `Bool' 
     `a' is a rigid type variable bound by 
      the type signature for `foo' at poly.hs:1:14 
    In the first argument of `f', namely `True' 
    In the expression: f True 
    In the expression: if n > 0 then f True else f x 

poly.hs:2:40: 
    Couldn't match expected type `Bool' against inferred type `c' 
     `c' is a rigid type variable bound by 
      the type signature for `foo' at poly.hs:1:34 
    In the first argument of `f', namely `x' 
    In the expression: f x 
    In the expression: if n > 0 then f True else f x 

이 무엇을 의미합니까? Rank-N 다형성이 유효하지 않습니까? (면책 조항 : 저는 Haskell 프로그래머가 아닙니다. 그러나 OCaml은 그러한 명시적인 타입 서명을 지원하지 않습니다.)

Answer 1

코드에서 실제로 rank-N 다형성을 사용하지 않습니다.

foo :: forall a. forall b. forall c. (a -> b) -> c -> Integer -> b 

이것은 일반적인 rank-1 유형입니다. 그것은 읽습니다 : forall a, b and c이 함수는 a -> b 유형의 값, c 유형의 값 및 Integer의 값을 가지며 b 유형의 값을 반환합니다. 즉, 형식이 Bool -> Integer이거나 유형이 Integer -> Integer 인 함수를 사용할 수 있다고합니다. 이 아니라은 함수가 인수에서 다형성을 가져야한다고 말합니다. 그런 말을하려면 사용할 필요가 : 당신은 함수의 유형 b가 고정되어 forall a. a -> b을 할 필요가 있다는 말을하는지

이제

foo :: forall b. forall c. (forall a. a -> b) -> c -> Integer -> b 

하지만 a는 새로 도입 된 변수이기 때문에 함수가 필요 그것의 논쟁에서 다형성을 가져라.