如何为具有非*类型幻影类型参数的GADT派生Eq

Question

例如，尝试编译以下代码

{-# LANGUAGE StandaloneDeriving, KindSignatures, DataKinds, GADTs#-}

data ExprTag = Tag1 | Tag2

data Expr (tag :: ExprTag) where
  Con1 :: Int -> Expr tag
  Con2 :: Expr tag -> Expr tag
  Con3 :: Expr tag -> Expr Tag2

deriving instance Eq (Expr a)

给出一个类型错误

Could not deduce (tag1 ~ tag)
from the context (a ~ 'Tag2)
  bound by a pattern with constructor
             Con3 :: forall (tag :: ExprTag). Expr tag -> Expr 'Tag2,
           in an equation for `=='
  at Bar.hs:11:1-29
or from (a ~ 'Tag2)
  bound by a pattern with constructor
             Con3 :: forall (tag :: ExprTag). Expr tag -> Expr 'Tag2,
           in an equation for `=='
  at Bar.hs:11:1-29
  `tag1' is a rigid type variable bound by
         a pattern with constructor
           Con3 :: forall (tag :: ExprTag). Expr tag -> Expr 'Tag2,
         in an equation for `=='
         at Bar.hs:11:1
  `tag' is a rigid type variable bound by
        a pattern with constructor
          Con3 :: forall (tag :: ExprTag). Expr tag -> Expr 'Tag2,
        in an equation for `=='
        at Bar.hs:11:1
Expected type: Expr tag1
  Actual type: Expr tag
In the second argument of `(==)', namely `b1'
In the expression: ((a1 == b1))
When typechecking the code for  `=='
  in a standalone derived instance for `Eq (Expr a)':
  To see the code I am typechecking, use -ddump-deriv

我可以理解为什么这不起作用，但是有什么解决方案不需要我手动编写Eq (和Ord)实例吗？

Answer 1

正如其他人所认识到的那样，问题的关键是Con3类型中存在的量化tag。当你试图定义

Con3 s == Con3 t = ???

没有理由s和t应该是具有相同tag的表达式。

但也许你并不关心？您可以很好地定义异构相等性测试，它可以很好地比较Expr的结构，而不管标签是什么。

instance Eq (Expr tag) where
  (==) = heq where
    heq :: Expr a -> Expr b -> Bool
    heq (Con1 i) (Con1 j) = i == j
    heq (Con2 s) (Con2 t) = heq s t
    heq (Con3 s) (Con3 t) = heq s t

如果您确实关心，那么建议您为Con3配备一个存在量化的tag的运行时见证。实现这一点的标准方法是使用单例构造。

data SingExprTag (tag :: ExprTag) where
  SingTag1 :: SingExprTag Tag1
  SingTag2 :: SingExprTag Tag2

对SingExprTag tag中值的案例分析将准确地确定tag是什么。我们可以将这段额外的信息添加到Con3中，如下所示：

data Expr' (tag :: ExprTag) where
  Con1' :: Int -> Expr' tag
  Con2' :: Expr' tag -> Expr' tag
  Con3' :: SingExprTag tag -> Expr' tag -> Expr' Tag2

现在我们可以检查标签是否匹配。我们可以像这样为标记单例编写异构相等...

heqTagBoo :: SingExprTag a -> SingExprTag b -> Bool
heqTagBoo SingTag1 SingTag1 = True
heqTagBoo SingTag2 SingTag2 = True
heqTagBoo _        _        = False

这样做的...but将是完全无用的，因为它只给我们一个Bool类型的值，而不知道这个值意味着什么，也不知道它的真实情况会赋予我们什么。知道heqTagBoo a b = True没有告诉类型检查器任何关于a和b见证的标记的有用信息。布尔值没有多少信息。

我们可以编写本质上相同的测试，但在肯定的情况下提供一些证据，证明标签是相等的。

data x :=: y where
  Refl :: x :=: x

singExprTagEq :: SingExprTag a -> SingExprTag b -> Maybe (a :=: b)
singExprTagEq SingTag1 SingTag1  = Just Refl
singExprTagEq SingTag2 SingTag2  = Just Refl
singExprTagEq _        _         = Nothing

现在我们用汽油做饭了！我们可以为Expr'实现一个Eq实例，它使用ExprTag比较来证明在标记匹配时对两个Con3'子级的递归调用是合理的。

instance Eq (Expr' tag) where
  Con1' i    ==  Con1' j    = i == j
  Con2' s    ==  Con2' t    = s == t
  Con3' a s  ==  Con3' b t  = case singExprTagEq a b of
    Just Refl -> s == t
    Nothing -> False

一般情况是，提升的类型需要它们关联的单例类型(至少在我们获得适当的∏类型之前)，我们需要为这些单例家族生成证据的异构等价性测试，以便我们可以比较两个单例，并在它们见证相同的类型级值时获得类型级知识。然后，只要您的GADT为任何存在项携带单例见证，您就可以均匀地测试等价性，确保单例测试的肯定结果为其他测试提供统一类型的好处。

Answer 2

这是一个存在的问题，而不是提升的那种。在这种情况下，一种解决方案是提供非类型化表示

data UExpr = UCon1 Int | UCon2 UExpr | UCon3 UExpr deriving (Eq, Ord)

然后你只需要一个函数

toUExpr :: Expr t -> UExpr
toUExpr (Con1 x) = UCon1 x
        (Con2 x) = UCon2 $ toUExpr x
        (Con3 x) = UCon3 $ toUExpr x

而且很容易定义您想要的实例

instance Eq (Expr x) where
   (==) = (==) `on` toUExpr

instance Ord (Expr x) where
   compare = compare `on` toUExpr

要做得更好，几乎肯定需要模板Haskell。