如何将两个类型约束与逻辑或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也满足,则会违反开放世界的假设; 任何冲突解决规则都必然会导致添加实例以更改现有代码的行为.

也就是说,采摘R时b满意的,但a没有打破开放世界的假设,因为它涉及决定是一个实例是不是满意; ¹即使您添加了"两个满意的"构造函数,您也可以使用它来决定实例是否不存在(通过查看是否获得一个L或一个实例R).

因此,我不相信这样的或约束是可能的; 如果你可以观察到你得到的实例,那么你可以通过添加一个实例创建一个行为改变的程序,如果你不能观察到你得到的实例,那么它就没用了.

¹此实例和正常实例分辨率之间的差异(也可能失败)通常是编译器无法确定是否满足约束; 在这里,您要求编译器确定不能满足约束.一个微妙但重要的区别.