유형의 추론

Question

GHC가 유추해야한다고 생각하는 유형 서명을 원했습니다. 나는 거의 확실하게 의미있는 것은 (내가 좋아하는 종류에 그것을 실행하지 않는 것이 좋습니다)하지 않습니다 어떤이, 내 예를 최소화 : y의 정의에 유형 서명없이

{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, 
      TypeOperators, NoMonomorphismRestriction #-} 
module Foo where 

import Data.Typeable 

data Bar rp rq 

data Foo b = Foo (Foo b) 


rebar :: forall rp rq rp' rp'' . (Typeable rp', Typeable rp'') 
    => Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq) 
rebar p1 p2 (Foo x) = 
    -- The signature for y should be inferred... 
    let y = rebar p1 p2 x -- :: Foo (Bar rp rq) 
    -- The case statement has nothing to do with the type of y 
    in case (eqT :: Maybe (rp' :~: rp'')) of 
    Just Refl -> y 

를, 나는 오류가 발생합니다 :

Foo.hs:19:20: 
    Couldn't match type ‘rq0’ with ‘rq’ 
     ‘rq0’ is untouchable 
     inside the constraints (rp' ~ rp'') 
     bound by a pattern with constructor 
        Refl :: forall (k :: BOX) (a1 :: k). a1 :~: a1, 
       in a case alternative 
     at testsuite/Foo.hs:19:12-15 
     ‘rq’ is a rigid type variable bound by 
      the type signature for 
      rebar :: (Typeable rp', Typeable rp'') => 
         Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq) 
      at testsuite/Foo.hs:12:20 
    Expected type: Foo (Bar rp rq) 
     Actual type: Foo (Bar rp rq0) 
    Relevant bindings include 
     y :: Foo (Bar rp rq0) (bound at testsuite/Foo.hs:16:7) 
     rebar :: Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq) 
     (bound at testsuite/Foo.hs:14:1) 
    In the expression: y 
    In a case alternative: Just Refl -> y 
Failed, modules loaded: none. 

여러 occassions에에 지칠대로 지친 단사 사상 제한에 의해 체포 된 데, 나는 NoMonomorphismRestriction 켜져 있지만,이 동작을 변경하지 않습니다.

y의 유형이 함수의 출력 유형으로 추정되지 않는 이유는 무엇입니까?

Answer 1

monomorphism 제한은 최상위 바인딩에만 적용됩니다. 컴파일러는 y의 실제 유형을 알고 있지만, 그것에 대한 단일 유형을 유추 할 수있는 방법은 없습니다. 이것이 유형 오류의 원인입니다.단일 양식 바인딩을 해제하려면 올바른 확장자를 사용해야합니다.

{-# LANGUAGE NoMonoLocalBinds #-} 

이 코드를 사용하면 코드가 컴파일됩니다.

monomorphic let 바인딩에 대한 자세한 내용은 see the ghc wiki을 참조하십시오.

Answer 2

저는 GHC의 타이핑 알고리즘에 익숙하지 않습니다. 아직도, 컴파일러가 그것을 이해할 수없는 이유에 대한 나의 추측이 있습니다. Refl 일치하는 말 Char ~ rq 따라서, y 증명 올바른 반환형 Foo (Bar rp rq)을 갖기 때문에,

rebar :: forall rp rq rp' rp'' . (Typeable rp', Typeable rp'') 
    => Proxy rp' -> Proxy rp'' -> Foo rp -> Foo (Bar rp rq) 
rebar p1 p2 (Foo x) = 
    let y = ... :: Foo (Bar rp Char) 
    in case (eqT :: Maybe (Char :~: rq)) of 
    Just Refl -> y 

이 컴파일해야

이 코드를 고려한다. 프로그램은 유형 검사를 통과합니다.

그러나, y 이미 올바른 유형을 가지고, 우리가 대신이 경우

let y = ... :: Foo (Bar rp rq) 

이 있다고 가정하고, Refl는 쓸모가 없다. 다시 프로그램은 유형 검사를 통과합니다.

이제 이없고 유형 주석이 있다고 가정합니다. 컴파일은 어떻게 올바른 유형의 let y = ... 바인딩 알아낼 것인가? 결국, 을 (적어도) 두 사람이 전체 rebar의 정확한 타이핑에 이르게합니다.

_ -> y을 추가하면 왜 작동하는지 설명 할 수 있습니다.이 경우 컴파일러는 Refl이 필요하지 않음을 알고 있습니다. 대신 y -> error ""을 추가하면 y에 대한 정보를 얻을 수 없습니다.

실제 전체 기사는 위의 내용보다 복잡 할 수 있습니다. 여기서는 y의 정보 (즉, rebar p1 p2 x)를 편리하게 무시합니다. 다른 말로하면, 컨텍스트가 y에있는 정의에 대한 제약 조건 만 고려하고 다른 방향으로가는 제약 조건은 고려하지 않습니다.

예를 들어 유형 수식은 실제로는 rp' ~ rp''입니다.이 유형은 wr.r.t와는 무관합니다. 끝에 y 유형 어쩌면 컴파일러는 그것을 이해할만큼 똑똑하지 않을 수도 있습니다.