"开放世界假设"有什么用处？"

Question

"开放世界假设"有什么用处？"

4

作为一个（有点牵强附会的）例子，假设我想使用泛型来确定一个类型是否是无人居住的（没有非底部值）。在大多数情况下，我可以很好地解决这个问题：

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或GAbsurd b中的一个来实现GAbsurd (a :*: 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也应该有所有导入模块的列表吧？

- fluffyyboii

2

https://dev59.com/6cPra4cB1Zd3GeqPoMi_#71284052 - leftaroundabout

GHC 可能有一个导入模块列表，列出了该模块所依赖的模块，但是请想象一下，如果这段代码出现在一个库中，而该库随后被其他地方导入，那么就会有更多、新的依赖关系。 - Louis Wasserman

一个选择是使用一种开放类型族，指示每个类型是否为“Absurd”，以及每个表示是否为“GAbsurd”。然后您可以计算要采取哪条路径。当然，这意味着您处理的所有内容都需要一个实例。 - dfeuer

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- K. A. Buhr · Accepted Answer

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

我认为主要问题是在面对约束分离时，维护实例定义的连贯性和编译效率变得异常困难。问题在于你想象中语法中的假设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实例，我们可能会遇到真正的问题。

为了保持连贯性，基本上必须携带大量的额外类型信息，以解决在选择实例时的析合。我们可能不得不在运行时传递该信息并评估它，否则甚至对于相当琐碎的程序，我们可能会产生指数级别的专门实例。