从 GADT 推导出一个平凡的 Eq class

Question

我认为 GADT 很棒，直到我尝试使用散布在 Internet 上的任何 "expressions with GADTs" 示例。

传统的 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

传统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

仅强制执行 compared 的两个值 Expr 具有相同的类型并且是 Eq，但它不会告诉您有关不同表达式的类型。

从 GADT 推导出一个平凡的 Eq class

Deriving a trivial Eq class from a GADT

haskell

typeclass

gadt