Haskell에서의 모험 : GADT 's : 왜 다음과 같은 형 검사를합니까?

Question

다음은 GADT 's의 Simon Peyton-Jones가 작성한 this lecture입니다.

data T a where 
    T0 :: Bool -> T Bool 
    T1 :: T a 

를 그리고 요구되는 문제는 다음과 같은 기능의 유형입니다 무엇 :이 다음 데이터 형 선언 나에게

f x y = case x of 
      T0 _ -> True 
      T1 -> y 

는, 그것만이 가능한 유형은 보인다 이다 : 그러나

f :: T a -> Bool -> Bool 

, 다음과 같은 유형 :

f :: T a -> a -> a 

도 유효합니다!

f (T1) "hello" 

내 질문은 왜 유효 f의 두 번째 유형의 서명입니다 다음과 같이 그리고 실제로 당신은 f를 사용할 수 있을까?

Answer 1

일반적으로

case e of 
    K1 ... -> e1 
    K2 ... -> e2 
    ... 

는 모든 표현이 일반적인 유형을 공유 ei 필요가있다 확인 입력합니다.

GADT를 사용하는 경우에도 마찬가지입니다. 단, 각 분기에서 생성자는 해당 분기에서 보유하는 것으로 알려진 일부 유형 항등식 T ~ T'을 제공합니다. 따라서 모든 ei이 공통 유형을 공유하는지 확인하면 더 이상 유형 유형이 동일하지 않아도되지만 유형 방정식이 유지 될 때만 동일해야합니다.특히

:

이

f :: T a -> a -> a 
f x y = -- we know x :: T a , y :: a 
    case x of 
     T0 _ -> -- provides a ~ Bool 
       True -- has type Bool 
     T1 -> -- provides a ~ a (useless) 
       y  -- has type a 

여기에 우리가 일반적으로 잘못된 것 Bool ~ a를 확인해야하지만, 우리는 제공된 평등 a ~ Bool에서이를 확인할 필요가 있기 때문에 여기에 진실이된다. 그리고, 그런 경우에, 그것은 사실이됩니다!

는 (솔직히 말해서, 타입 시스템은 약간 다른 것으로, 두 가지) 그들의 알려진 등식에서 서명 (에 선언 된 유형에 동일한 아닌 경우 확인 않습니다 -.하지만 제가 간단하게하자를 GADT 들어 그러한 서명과 일치하는 패턴은 항상 어떤 형식으로 필요합니다.)

이것은 GADT의 전체 요점입니다.이 패턴은 브랜치에 다른 유형이있는 패턴 일치를 유형 체크 할 수 있습니다.

Answer 2

는 f의 정의 두 가지 경우가 있습니다 둘 다 두 번째 유형의 서명과 일치 :

여기

T0 _ -> True 

당신의 인수는 유형 T Bool이었다 당신의 결과는 Bool이다. 그래서 이것은 a ~ Bool에 대한 당신의 타입 서명과 일치합니다.

다음

T1 -> y 

당신의 인수는 유형 T a이었다 당신의 결과는 유형 a의 인 y이다. 따라서 이것은 a에 대한 서명과 일치합니다.

이것이 유형 안전 이유를 이해하려면 자신에게 다음 질문을하십시오. f으로 전화하여 결과가 유형 서명과 일치하지 않을 수있는 방법이 있습니까? T a과 a을 전달한 경우 a이 아닌 다른 것을 다시 얻을 수 있습니까?

그리고 대답은 다음과 같습니다. 아니오, 없습니다. T0 (a이 Bool 인 경우)을 전달하면 Bool이 표시됩니다. T1을 전달하면 a 유형으로 보장되는 두 번째 인수가 반환됩니다. f (T1 :: T Int) "notAnInt"과 같이 호출하려고하면 형식이 일치하지 않기 때문에 컴파일되지 않습니다. 즉 : 형식 서명과 일치하는 함수의 모든 응용 프로그램은 서명에 따라 올바른 결과 형식을 생성합니다. 따라서 f은 유형 안전합니다.