1

I understand the following type family shouldn't and perhaps can't be implemented in GHC:

type family MatchesConstraint c a :: Bool where
  MatchesConstraint c a is True if (c a)
  MatchesConstraint c a is False otherwise

This is problematic because classes are open, so MatchesConstraint c a could evaluate to True for some parts of the program and False in others depending on what instances are in scope, which I imagine could be potentially quite disastrous.

But consider the following:

type family MatchesConstraint c a :: Bool where
  MatchesConstraint c a is True if (c a)
  MatchesConstraint c a doesn't reduce otherwise

This seems quite safe. In some parts of our program we might fail to reduce if an instance is not in scope, but we'll never have an inconsistency.

Can I make something like this work in GHC?

The reason I'm asking for this, is because one could perhaps select instances based on not just type directly but class. Which could be a useful thing in some contexts I believe.

4

1 回答 1

0

我在咖啡馆回答了你的一个类似问题。

正如@Carl 所说，所有实例都应该在任何地方都在范围内。例外是编译所谓的“孤儿实例” ——这是一件坏事，很容易避免。

对于此处的记录，该方法是在您的类中使用 Associated 类型，并具有默认定义。如果您真的很高兴 Associated 类型在与约束不匹配的情况下抛出“无实例”错误，则此方法有效：

class A t where
  type MatchesA t :: Bool           -- Associated type
  type instance MatchesA t = True   -- default instance
  ...                               -- methods for A

instance A Int where
                                    -- uses default instance for MatchesA
  ...                               -- method implementations as usual

-- undefined :: (MatchesA Int)      -- gives type True
-- undefined :: (MatchesA Bool)     -- gives 'no instance' error

我认为您可以获得一个非此即彼的约束——请参阅咖啡馆帖子中的 MatchesA 或 MatchesB。（我已经快速测试过了，它可能有点不稳定，这取决于类型族减少的渴望程度。）

你不能用这种方法做的是，如果约束成立，就选择一件事，如果不成立，就选择另一件事。所以你能得到的最好的就是“减少失败”。在咖啡馆帖子中，我使用更全面的方法链接到（相当旧的）wiki 页面，该方法依赖于重叠实例。关联类型不允许重叠:-(。

编辑：编译器不会按照您在评论中希望类的方式公开某些约束是否匹配，这有一个深刻的原因Prelude：您可能正在使用匹配的事实来选择另一个类的某个实例C；并且可能还有另一个类D，其实例选择取决于C匹配；和A, B的实例选择取决于D。所以现在我们有了循环依赖。这可能会因编译器尚未看到的其他模块中的其他实例而变得更加复杂。

因此，wiki 页面上所有那些（显然）重复的实例表示程序员知道所有实例以及它们如何相互依赖，编译器无法弄清楚。

于 2018-05-07T12:07:27.600 回答