开放世界假设有什么好处？

Question

作为一个（有点人为的）示例，假设我想使用泛型来确定类型何时无人居住（通过非底值）。我可以很好地完成大部分工作：

class Absurd a where
    absurd :: a -> b
    default absurd :: (Generic a, GAbsurd (Rep a)) => a -> b
    absurd = gabsurd . from
class GAbsurd f where
    gabsurd :: f p -> b
instance GAbsurd f => GAbsurd (M1 i c f) where
    gabsurd (M1 x) = gabsurd x
instance Absurd c => GAbsurd (K1 i c) where
    gabsurd (K1 x) = absurd x
instance GAbsurd V1 where
    gabsurd = \case
instance (GAbsurd a, GAbsurd b) => GAbsurd (a :+: b) where
    gabsurd (L1 x) = gabsurd x
    gabsurd (R1 x) = gabsurd x

当我需要为 :*: 定义一个实例时，问题就出现了。实现 GAbsurd (a :*: b) 只需要 GAbsurd a 或 GAbsurd b 之一，但是我能做的最好的就是两者都需要，这太强了。例如：

data Void
data X = X Char Void

显然 X 是一个“荒谬”的类型，但这不能推断，因为虽然 Void 是荒谬的，但 Char 却不是，并且所以约束(Absurd Char, Absurd Void)无法解决。

我想做的是使用某种“约束析取”，如下所示：

instance (GAbsurd a || GAbsurd b) => GAbsurd (a :*: b) where
    gabsurd (x :*: y) = case eitherConstraint of
        LeftC  -> gabsurd x
        RightC -> gabsurd y

但是，在开放世界假设下， 这是不可能的。事实上，Data.Boring 中的代码（也包含 Absurd）完全忽略了这个问题：

GAbsurd (f :*: g) 有两个合理的实例，因此我们两者都没有定义

因此这引出了我的问题：为什么开放世界假设如此重要？我最好的猜测是它与孤立实例有关，但即便如此，GHC 不应该有所有导入模块的列表吗？

Answer 1

我不确定关键问题是孤儿实例和模块。

我认为主要问题是，面对约束析取时，要保持实例定义的连贯性和编译效率的连贯性是很难的。问题在于，您想象中的语法中的假设要么在编译时本地解决。例如，考虑函数：

foo :: (GAbsurd a) => GAbsurd (a :*: b)
foo = gabsurd

bar :: (GAbsurd b) => GAbsurd (a :*: b)
bar = gabsurd

这些都是类型纠正的。在每种情况下，都需要gabsurd（a：*：b）实例，并且可以通过gabsurd a 或gabsurd b。但是，使用gabsurd（a：*：b）= gabsurd a的明显的编译时，实际实现这些功能的本地解决方案，用于第一个和gabsurd（a：*：*：*：*：*：*：*：*：b） ）= gabsurd b第二个导致不一致。这不是这个特定示例的问题，但是如果这些是ord实例，并且我们使用一个多态函数将对象插入set和另一个多态函数，以将对象查看对象在那个set中，如果他们最终使用两种不同的ord实例，我们可能会遇到一个真正的问题。

为了保持连贯性，我们基本上必须随身携带许多其他类型的信息，以在选择实例时解决析取。而且，我们可能必须在传递这些信息和在运行时进行评估之间进行选择，或者为即使是非常琐碎的程序生成指数级的专业实例。