GADT에서 사소한 Eq 클래스를 파생합니다.

Question

인터넷을 통해 흩어져있는 "GADT가있는 표현식"을 사용할 때까지 GADT가 훌륭하다고 생각했습니다.

전통적인 ADT는 무료로 Eq로 간주하여 정의 평등을 제공합니다. (매우 당연하게도) 내가 얻을

data Expr a where 
    (:+:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a 
    (:-:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a 
    (:*:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a 
    (:/:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a 
    (:=:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool 
    (:<:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool 
    (:>:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool 
    (:>=:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool 
    (:<=:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool 
    (:<>:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool 
    EOr :: Expr Bool -> Expr Bool -> Expr Bool 
    EAnd :: Expr Bool -> Expr Bool -> Expr Bool 
    ENot :: Expr Bool -> Expr Bool 
    ESymbol :: (Show a, Eq a) => String -> Expr a 
    ELiteral :: (Show a, Eq a) => a -> Expr a 
    EFunction :: (Show a, Eq a) => String -> [Expr a] -> Expr a 
    deriving (Eq) 

:

• Can't make a derived instance of ‘Eq (Expr a)’: 
     Constructor ‘:+:’ has existentials or constraints in its type 
     Constructor ‘:-:’ has existentials or constraints in its type 
     Constructor ‘:*:’ has existentials or constraints in its type 
     Constructor ‘:/:’ has existentials or constraints in its type 
     Constructor ‘:=:’ has existentials or constraints in its type 
     Constructor ‘:<:’ has existentials or constraints in its type 
     Constructor ‘:>:’ has existentials or constraints in its type 
     Constructor ‘:>=:’ has existentials or constraints in its type 
     Constructor ‘:<=:’ has existentials or constraints in its type 
     Constructor ‘:<>:’ has existentials or constraints in its type 
     Constructor ‘EOr’ has existentials or constraints in its type 
     Constructor ‘EAnd’ has existentials or constraints in its type 
     Constructor ‘ENot’ has existentials or constraints in its type 
     Constructor ‘ESymbol’ has existentials or constraints in its type 
     Constructor ‘ELiteral’ has existentials or constraints in its type 
     Constructor ‘EFunction’ has existentials or constraints in its type 
     Possible fix: use a standalone deriving declaration instead 
    • In the data declaration for ‘Expr’ 

나는 각 생성자에 대한 Eq 제한을하지 않았다면 이해할 수 있지만, 지금은 사소한 평등을 작성해야이 코드에 대한 GADTs에서 모든 생성자에 대한 규칙. 내가

Answer 1

전통적인 deriving가 GADT 제약을 처리 할 수있는 것보다 이것에 대해 갈 수있는 더 좋은 방법이 같은

는 느낌. 원칙적으로 할 수있는 독립 유도하는, 그러나

{-# LANGUAGE GADTs, StandaloneDeriving #-} 
data Expr a where 
    (:+:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a 
    ... 
deriving instance Eq (Expr a) 

, 그 Eq 인스턴스가 단지 수 없기 때문에 도움이되지 않습니다. 어떻게 비교 하시겠습니까

(1 :<: (2 :: Expr Int)) == (pi :<: (sqrt 2 :: Expr Double)) 

그것은 단지 불가능합니다. GADT 제약

(:<:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr Bool 

는 해당 Expr 동일한 유형을 가지고 Eq입니다 모두 값 비교 수 있는지 확인합니다,하지만 당신에게 다른 표현의 유형에 대해 아무것도 말해주지 않습니다.