Получение тривиального класса Eq из GADT

Question

Я думал, что GADT были великолепны, пока я не попытался применить примеры «выражения с GADT», разбросанные по всему Интернету.

Традиционные ADT любезно предоставляют определение равенства в виде Eq бесплатно. В GADTs для этого кода:

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 ограничение для каждого конструктора, но теперь я должен написать тривиальное равенство правила для всех этих конструкторов.

Я чувствую, что есть лучший способ пойти об этом, чем я

Answer 1

Традиционная deriving не может справиться с GADT ограничений. Standalone, происходящий, в принципе:

{-# 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, но это не говорит вам что-нибудь о типах различных выражений.