haskell - 如何使用非 * 类型的幻影类型参数为 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

正如其他人所指出的，问题的关键是存在量化 tag在 Con3 的类型中.当你试图定义

Con3 s == Con3 t = ???

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

但也许你不在乎？您可以很好地定义异构相等性测试，它很高兴进行比较 Expr s 在结构上，与标签无关。

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

...但这样做完全没用，因为它只给我们一个 Bool 类型的值。 ，不知道这个值(value)意味着什么，也不知道它的真相可能赋予我们什么。知乎 heqTagBoo a b = True没有告诉类型检查器任何关于 a 的标签有用的信息和 b证人。 bool 值有点无意义。

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

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

现在我们用煤气做饭!我们可以实现一个 Eq 的实例为 Expr'使用 ExprTag比较以证明对两个 Con3' 的递归调用是合理的当标签显示匹配时， child 。

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 携带任何存在的单例见证，您就可以均匀地测试相等性，确保单例测试的积极结果为其他测试提供统一类型的奖励。