haskell - 从 GADT 派生一个简单的 Eq 类

Question

我认为 GADT 很棒，直到我尝试使用散布在互联网上的任何“带有 GADT 的表达式”示例。

传统的 ADT 以 Eq 的形式免费提供定义相等性。在此代码的 GADT 中:

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

传统派生无法处理 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，但它不会告诉您任何有关不同表达式的类型。