从GADT中派生一个平凡的Eq类

Question

我认为GADT非常棒，直到我试图将任何“GADTs”表达式分散在互联网上使用的例子。

传统的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约束。独立推导，原则：

{-# 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，但它不会告诉你的类型的不同表达什么。