如何使用非*幻像幻像类型参数导出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,无论标签如何,都可以在结构上进行比较.

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,不知道这个价值意味着什么,也不知道它的真理可能赋予我们什么.知道这heqTagBoo a b = True并没有告诉typechecker任何有用的标签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

现在我们用煤气做饭!我们可以实现一个使用比较的实例,Eq以便在标记显示匹配时证明两个子节点上的递归调用.Expr'ExprTagCon3'

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

要做得更好几乎肯定需要 Template Haskell。