하스켈에게`(Reverse (Reverse xs)) ~ xs`를 알려 줌

Question

Reverse :: [k] -> [k]이 타입 패밀리라면, 하스켈은 (Reverse (Reverse xs)) ~ xs을 말할 수 없다. 유형 시스템에 런타임 비용없이 이것을 알릴 수있는 방법이 있습니까?

나는 단지 unsafeCoerce을 사용하고 싶지만 유감 스럽습니다.

Answer 1

GHC에서 ~의 동작에 영향을 줄 수있는 유일한 방법은 실제로 a :~: b (또는 이와 유사한 것으로)의 인스턴스를 구성하는 것입니다 (중요한 것은 typechecker에 "증명"하는 용어를 만드는 것입니다). 그런 다음 패턴 일치가 Refl 생성자에서 발생합니다. 이는 런타임에 증명 증인을 평가해야합니다. 내 이해는 GHC의 종속 유형에 대한 현재 설계가 여전히 유형 평등의 모든 증명을 실행해야 할 것입니다. 그러나 유형 검사를 한 후에 GHC의 재 작성 규칙을 사용하여 평가 증인을 매우 저렴한 비용으로 만들지 만 여전히 안전하다고 증명할 수있는 매우 저렴한 비용의 기능 (예 : unsafeCoerce Refl :: Reverse (Reverse a) :~: a)으로 대체 할 수 있습니다 (증인이 이미 유형 검사를 받았으므로, 그것이 끝나면 정확한 증거를 산출한다는 것을 보여줍니다). 하스켈에 따라 입력의 현재 상태에 대한

많은 자세한 내용은 여기에서 찾을 수 없습니다 : https://typesandkinds.wordpress.com/2016/07/24/dependent-types-in-haskell-progress-report/