유형에 대한 의 실체 적 정량은 무엇이며 무엇을 사용할 수 있는지에 대한 일반적인 생각이 있습니다. 그러나 지금까지 경험 한 바에 따르면 개념을 효과적으로 사용하기 위해서는 이해해야 할 많은주의 사항이 있습니다.하스켈의 실존 적 정량화 자세히
질문 : GHC에서 실존 적 수량화가 어떻게 구현되는지 설명하는 훌륭한 자료가 있습니까? 나는.
내 목표는 GHC가 내게 던지는 오류 메시지를 더 잘 이해하는 것입니다. 메시지는 대개 "this type using forall and this other type don't match" 행을 따라 말합니다. 그러나 왜 그런지 설명하지 않습니다.
자세한 내용은 Simon Peyton-Jones의 논문에서 다루지 만, 기술적 전문 지식이 풍부해야 이해할 수 있습니다. Haskell 타입 추론이 어떻게 작동하는지에 대한 논문을 읽고 싶다면, 실존 타입을 다른 여러가지 특징과 결합하는 일반화 된 대수 데이터 타입 (GADTs)에 대해 읽어야합니다. http://research.microsoft.com/en-us/people/simonpj/에있는 논문 목록에있는 "GADT에 대한 완전하고 결정적인 유형 추론"을 제안합니다.
실존 양론은 보편적 인 양화와 같이 실제로 작동합니다. 다음은이 둘 사이의 유사점을 강조하는 예입니다. useExis 함수는 쓸모가 없지만 여전히 유효한 코드입니다. 먼저
data Univ a = Univ a
data Exis = forall a. Exis a
toUniv :: a -> Univ a
toUniv = Univ
toExis :: a -> Exis
toExis = Exis
useUniv :: (a -> b) -> Univ a -> b
useUniv f (Univ x) = f x
useExis :: (forall a. a -> b) -> Exis -> b
useExis f (Exis x) = f x
는 toUniv 및 toExis 거의 동일 있습니다. 두 데이터 생성자 모두 다형이기 때문에 둘 다 자유 형식 매개 변수 a을가집니다. 반환 유형이 toUniv 인 a이 나타나지만 반환 유형 toExis에는 표시되지 않습니다. 데이터 생성자를 사용할 때 발생할 수있는 유형 오류 유형에 관해서는 실존 유형과 범용 유형간에 큰 차이가 없습니다.
둘째, 순위 2 유형 forall a. a -> b은 useExis입니다. 이것이 타입 유추의 큰 차이점입니다. 패턴 일치 (Exis x)에서 가져온 실존 유형은 함수 본문에 전달 된 추가 숨김 유형 변수와 같은 역할을하며 다른 유형과 통합해서는 안됩니다. 이를 명확히하기 위해, 여기에 통합되지 않아야하는 유형을 통합하려고하는 마지막 두 함수의 잘못된 선언이 있습니다. 두 경우 모두 x의 유형이 관련되지 않은 유형 변수와 통합되도록합니다. useUniv에서 유형 변수는 함수 유형의 일부입니다. useExis에서는 데이터 구조의 실존 유형입니다.
useUniv' :: forall a b c. (c -> b) -> Univ a -> b
useUniv' f (Univ x) = f x -- Error, can't unify 'a' with 'c'
-- Variable 'a' is there in the function type
useExis' :: forall b c. (c -> b) -> Exis -> b
useExis' f (Exis x) = f x -- Error, can't unify 'a' with 'c'.
-- Variable 'a' comes from the pattern "Exis x",
-- via the existential in "data Exis = forall a. Exis a".