强制 GHC 忽略缺少的类型约束

Question

我使用构造函数子类型构建了一个类型 Sup，它嵌入了另一个类型 t 的值。

data Sup t = ...
           | Sub t 
           deriving Eq

因为Sup 省略的部分包含很多构造函数，没有一个使用t，我想派生 Eq (Sup t) 而不是手动实例。

类型约束 Eq t 现在已在 (==) 的实例上针对 Sup t：

(==) :: Eq t => Sup t -> Sup t -> Bool

谓词isSub :: Sup t -> Bool定义如下：

isSub :: Sup t -> Bool
isSub (Sub _) = True
isSub _       = False

借助这个谓词，我想定义以下运算符：

supEq :: Sup t -> Sup t -> Bool
supEq x y = not (isSub x) && not (isSub y) && x == y

GHC 不接受上述定义，因为缺少类型约束Eq t。但是，由于惰性求值，我知道 t 类型的值之间的相等性从未实际使用过。

有没有办法强制 GHC 忽略缺少的类型约束？ 或者，有没有一种方法可以定义Sup 或supEq 以获得所需的结果：supEq 的定义无需在使用supEq 的任何地方传播冗余类型约束，而无需提供手册例如Eq (Sup t)。

Answer 1

可能最简单的做法是定义一个自定义Eq (Sup t) 实例。

instance (Eq t) => Eq (Sup t) where
  (Sub a) == (Sub b) = a == b
  A == A = True
  ...

或者，如果您希望== 的行为类似于supEq（因此您根本不需要supEq），您可以编写没有约束的实例：

instance Eq (Sup t) where
  (Sub a) == (Sub b) = False
  A == A = True
  ...

另一种方法是将Sup t拆分为两种数据类型：

data Sup' = A | B | ... | Z deriving (Eq) -- nothing depends on `t`
data Sup t = Sub t | Sup'

supEq :: Sup t -> Sup t -> Bool
supEq (Sub _) _ = False
supEq _ (Sub _) = False
supEq a b = a == b

当然，最后一个选择是颠覆类型系统。这几乎可以肯定是错误的做法，但我会把这个决心留给你。

{-# LANGUAGE ScopedTypeVariables #-}
import Data.Constraint

supEq :: forall t . Sup t -> Sup t -> Bool
supEq x y = let Dict = unsafeCoerce (Dict :: Dict ()) :: Dict (Eq t)
            in not (isSub x) && not (isSub y) && x == y

Answer 2

当然，最简单的解决方案是将您的类型分成两种类型，正如其他人所建议的那样。但这会产生语法噪音——额外的构造函数。如果你想两者兼得，你可以使用reflection:

import Data.Reflection
import Data.Proxy 
import Data.Coerce 

data Sup t = Sub t | A | B | C | D | E -- .. etc
  deriving (Eq, Show) 

我们现在将生成的Eq 代码用于Sup，但在将Sub 与Sub 进行比较时，替换为不同的函数，而不是(==)。

首先您需要进行一些设置（我认为这应该在 reflection 包本身中 - 它具有 Monoid 和 Applicative 的类似代码）：

newtype ReifiedEq a = ReifiedEq { eq :: a -> a -> Bool } 
newtype ReflectedEq s a = ReflectedEq a 

instance Reifies s (ReifiedEq a) => Eq (ReflectedEq s a) where 
  (==) = coerce (eq (reflect (Proxy :: Proxy s))) 

这是解决方案的核心 - ReflectedEq s a 类型的值只是 a，但在比较相等时使用 Reifies 提供的相等函数，您可以随时指定。请注意，reflection 包使用类型级别机制来防止在同一上下文中使用多个 Eq 实例。

现在你可以编写一个比你想要的更通用的函数：

supEqWith :: (t -> t -> Bool) -> Sup t -> Sup t -> Bool 
supEqWith k x y = reify (ReifiedEq k) (\p -> h p x == h p y) where 
  h :: Proxy s -> Sup a -> Sup (ReflectedEq s a) 
  h _ = coerce 

此函数只是比较 Sup 值是否相等，使用指定函数 (k) 比较 Sub 中的 t 值。需要h函数正确指定幻像类型参数（s），否则会产生歧义。

您想要的功能很简单：

supEq = supEqWith (\_ _ -> False) 

Answer 3

如果您的Sup 类型可以是t 中的函子（deriving Functor 将适用于您给出的示例），并且您知道其他构造函数都没有使用t，那么您可以@ 987654325@它。

那么您就可以保证t 不会有趣地影响相等性检查，并且不需要原始的t 具有Eq。您只需要注意两个输入均为Sub _ 的情况，以便返回false 而不是true。

subEq (Sub _) _ = False
subEq _ (Sub _) = False
subEq x y = fmap (const ()) x == fmap (const ()) y

即使您不想让 Sup 成为仿函数，您仍然可以实现 submap :: (a -> b) ->Sup a -> Sup b 并使用它。

Answer 4

如果您使用(==) 并坚持使用不出所料的派生实例，则无法摆脱Eq 约束。此外，就supEq 而言，您的不变量没有被强制执行（考虑如果您犯了错误并在isSub 中交换True 和False 会发生什么）。就Sup 模式匹配而言，您可能最好写supEq：

data Sup t = Foo
           | Bar
           | Sub t 
           deriving Eq

supEq :: Sup t -> Sup t -> Bool
supEq (Sub _) _ = False
supEq _ (Sub _) = False
supEq Foo Foo = True
supEq Bar Bar = True
supEq _ _ = False

如果有足够多的情况导致以这种方式编写supEq 变得烦人，您可以将非Sub 情况拆分为单独的类型，如 crockeea 答案中倒数第二个示例所示，转载如下为了完整起见：

data Sup' = Foo | Bar deriving (Eq)
data Sup t = Sub t | NotSub Sup' deriving (Eq)

supEq :: Sup t -> Sup t -> Bool
supEq (Sub _) _ = False
supEq _ (Sub _) = False
supEq (NotSub a) (NotSub b) = a == b