5

例如，尝试编译以下代码

{-# 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）实例吗？

4

2 回答 2

17

正如其他人所指出的那样，问题的关键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

对 in 值的案例分析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

...但是这样做是完全没有用的，因为它只给了我们一个 type 的值Bool，不知道这个值意味着什么，也不知道它的真实性可能赋予我们什么。知道这heqTagBoo a b = True一点并不能告诉类型检查器关于标签 whicha和bwitness 的任何有用信息。布尔值有点缺乏信息。

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

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'

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

于 2012-11-17T13:30:20.237 回答
1

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

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

要做得比这更好，几乎可以肯定需要 Template Haskell。

于 2012-11-17T00:02:07.747 回答