데이터 유형이있는 GADT의 Haskell 패턴 일치

Question

데이터 유형과 GADT를 결합하는 것이 좋음을 알았습니다. 이전보다 (대부분의 용도로는 거의 Coq, Agda 등) 훨씬 더 안전합니다. 슬프게도, 가장 간단한 예제에서는 패턴 매칭이 실패하고 타입 클래스를 제외하고는 함수를 작성할 수 없다고 생각할 수 있습니다.

은 여기 내 슬픔을 설명하는 예입니다 :

data Nat = Z | S Nat deriving Eq 

data Le :: Nat -> Nat -> * where 
    Le_base :: Le a a 
    Le_S :: Le a b -> Le a (S b) 

class ReformOp n m where 
    reform :: Le (S n) (S m) -> Le n m 

instance ReformOp a a where 
    reform Le_base = Le_base 

instance ReformOp a b => ReformOp a (S b) where 
    reform (Le_S p) = Le_S $ reform p 

class TransThm a b c where 
    trans :: Le a b -> Le b c -> Le a c 

instance TransThm a a a where 
    trans = const 

instance TransThm a a b => TransThm a a (S b) where 
    trans Le_base (Le_S p) = Le_S $ trans Le_base p 

instance (TransThm a b c, ReformOp b c) => TransThm a (S b) (S c) where 
    trans (Le_S p) q = Le_S $ trans p $ reform q 

우리는 두 종류의 클래스 (정리 하나, 유틸리티 작동하려면 하나의)와 5 개 인스턴스가 - 단지 사소한 정리를 위해. 호출 할 때

-- not working, I understand why 
trans :: Le a b -> Le b c -> Le a c 
trans Le_base Le_base = Le_base 
trans Le_base (Le_S p) = Le_S $ trans Le_base p 
trans (Le_S p) q = Le_S $ trans p $ reform q 

그리고 자신의 각 절을 유형 확인하고 (일치하도록 노력하고, 따라서 가치) 할 수있는 경우를 결정 당에 전화하는, 그래서하지 : 이상적으로, 하스켈은이 기능을 볼 수 있었다 trans Le_base Le_base Haskell은 첫 번째 경우 만 세 변수가 동일하다는 것을 알게되고 첫 번째 절에서만 일치를 시도합니다.

Answer 1

trans의 패턴 일치 정의가 Agda 또는 Coq에서 어떻게 작동하는지 알 수 없습니다. 당신이 대신 다음과 같은 작성하는 경우

이 작동 : 물론

reform :: Le (S n) (S m) -> Le n m 
reform Le_base   = Le_base 
reform (Le_S Le_base) = Le_S Le_base 
reform (Le_S (Le_S p)) = Le_S (reform (Le_S p)) 

trans :: Le a b -> Le b c -> Le a c 
trans Le_base q  = q 
trans (Le_S p) Le_base = Le_S p 
trans (Le_S p) (Le_S q) = Le_S (trans p (reform (Le_S q))) 

은 또한 더 직접적으로 정의 할 수 있습니다 : 사실

trans :: Le a b -> Le b c -> Le a c 
trans p Le_base = p 
trans p (Le_S q) = Le_S (trans p q)