Ableitung einer trivialen Eq-Klasse aus einer GADT

Question

Ich dachte GADTs waren großartig, bis ich versuchte, einige der "Ausdrücke mit GADTs" Beispiele über das Internet verteilt zu verwenden.

Traditionelle ADTs bieten freundlicherweise Definitionsgleichheit in Form von Eq kostenlos. In GADTs für diesen Code:

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) 

ich (sehr verständlich):

• 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’ 

was verständlich wäre, wenn ich für jeden Konstruktor nicht die Eq Einschränkung hatte, aber jetzt muss ich trivial Gleichheit schreiben Regeln für alle diese Konstruktoren.

Ich fühle mich wie es besseren Weg, um darüber zu gehen, als ich

Answer 1

Traditionelle deriving habe nicht GADT Einschränkungen umgehen. Standalone-Ableitungs können im Prinzip:

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

jedoch, dass Ihnen nicht helfen, weil die Eq Instanz einfach nicht möglich ist. Wie werden Sie vergleichen

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

Es ist einfach nicht möglich; die GADT Einschränkung

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

erzwingt nur, dass beide Werte verglichen, dass Expr die gleiche Art und sind Eq, aber es funktioniert nicht über die Arten von verschiedenen Ausdrücke sagen nichts.