如何将两个类型约束与 Haskell 中的逻辑或相结合

Question

在Haskell中，我们有能力将类型的约束与逻辑和相结合。

请考虑以下事项

type And (a :: Constraint) b = (a, b)

或更复杂的是

class (a, b) => And a b
instance (a, b) => And a b

我想知道如何在 Haskell 中逻辑或两个约束在一起。

我最接近的尝试是这个，但它并不完全有效。在这个尝试中，我用标签来定义类型约束，然后用隐式参数来定义它们。

data ROr a b where
 L :: a => ROr a b
 R :: b => ROr a b
type Or a b = (?choose :: ROr a b)
y :: Or (a ~ Integer) (Bool ~ Integer) => a
y = case ?choose of
 L -> 4
x :: Integer
x = let ?choose = L in y

它几乎可以工作，但用户必须应用最后一部分，编译器应该为我做到这一点。同样，当两个约束都满足时，这种情况不允许人们选择第三个选择。

如何在逻辑上或两个约束一起使用？

Answer 1

我相信

没有办法自动选择一个ROr a b;如果，例如 b很满意，但后来a也很满意;任何冲突解决规则都必然会导致添加实例以更改现有代码的行为。

也就是说，在b满意但a时选择R不会破坏开放世界的假设，因为它涉及确定实例不满意;¹ 即使您添加了"双方都满意"的构造函数，您也可以使用它来确定实例是否存在（通过查看您获得的是L还是R）。

因此，我不认为这样的 or 约束是可能的;如果你能观察你得到哪个实例，那么你可以通过添加一个实例来创建一个行为改变的程序，如果你不能观察你得到哪个实例，那么它就毫无用处。

¹ 此实例解析与正常实例解析（也可能失败）之间的区别在于，通常编译器无法确定是否满足约束;在这里，您要求编译器确定无法满足约束。一个微妙但重要的区别。

Answer 2

我来这里是为了回答你在咖啡馆的问题。不确定这里的q是否相同，但无论如何...

具有三个参数的类型类。

   class Foo a b c | a b -> c where
     foo :: a -> b -> c
   instance Foo A R A where ...
   instance Foo R A A where ...

除了功能依赖之外，我还想表达至少一个参数 a 和 b 是 c，

import Data.Type.Equality
import Data.Type.Bool
class ( ((a == c) || (b == c)) ~ True)
      => Foo a b c  | a b -> c  where ...

您需要打开一堆扩展程序。特别是UndecidableSuperClasses，因为类约束中的类型族调用在 GHC 可以看到的情况下是不透明的。

您的问题在这里

如何在逻辑上或两个约束一起使用？

要棘手得多。对于类型相等方法，==使用封闭类型族。所以你可以写一个封闭型族返回 kind Constraint ，但我怀疑有一个通用的解决方案。对于您的Foo课程：

type family AorBeqC a b c :: Constraint where
  AorBeqC a b a = ()
  AorBeqC a b c = (b ~ c)
class AorBeqC a b c => Foo a b c  | a b -> c  where ...

它可能具有不良和非对称类型的改进行为：如果GHC可以看到a, c是分开的，它将进入第二个方程并使用(b ~ c)来改善任何一个;如果它看不到它们是分开的，或者它们不可统一，它就会卡住。

通常，正如@ehird指出的那样，您无法测试约束是否不满足。类型相等性很特殊。