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

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

显然，CCD_；荒谬的"；类型，但这是无法推断的，因为尽管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

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

我认为主要的问题是，面对约束析取，要保持实例定义的一致性和编译的效率是出乎意料的困难。问题是，在您想象的语法中，假设的eitherConstraint不能在编译时简单地在本地解决。例如，考虑以下功能：

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实例，我们可能会遇到真正的问题。

为了保持一致性，在选择实例时，我们基本上必须携带大量额外的类型信息来解决析取问题。而且，我们可能不得不在传递信息和在运行时对其进行评估之间做出选择，或者为非常琐碎的程序生成指数数量的专用实例。