haskell - 为什么需要减少上下文？

Question

我刚刚阅读了this paper (Peyton Jones & Jones 的“类型类:对设计空间的探索”)，它解释了 Haskell 早期类型类系统的一些挑战，以及如何改进它。

他们提出的许多问题都与上下文减少有关，这是一种通过遵循“反向蕴涵”关系来减少对实例和函数声明的约束集的方法。

例如如果你有instance (Ord a, Ord b) => Ord (a, b) ...然后在上下文中，Ord (a, b)减少到 {Ord a, Ord b} (减少并不总是减少约束的数量)。

我从论文中不明白为什么有必要进行这种减少。

好吧，我收集到它是用来执行某种形式的类型检查的。当您拥有减少的约束集时，您可以检查是否存在一些可以满足它们的实例，否则会出现错误。我不太确定它的附加值(value)是什么，因为您会在使用现场注意到问题，但没关系。

但是即使你必须做那个检查，为什么要在推断类型中使用归约的结果呢？该论文指出它会导致不直观的推断类型。

这篇论文相当古老(1997 年)，但据我所知，上下文减少仍然是一个持续关注的问题。 Haskell 2010 规范确实提到了我在上面解释的推理行为 (link)。

那么，为什么要这样做呢？

Answer 1

我不知道这是否是必然的原因，但它可能被认为是一个原因:在早期的 Haskell 中，类型签名只允许具有“简单”约束，即应用于类型变量的类型类名称。因此，例如，所有这些都可以:

Ord a => a -> a -> Bool
Eq a => a -> a -> Bool
Graph gr => gr n e -> [n]

但这些都不是:

Ord (Tree a) => Tree a -> Tree a -> Bool
Eq (a -> b) => (a -> b) -> (a -> b) -> Bool
Graph Gr => Gr n e -> [n]

我认为当时有一种感觉——今天仍然如此——允许编译器推断一种无法手动编写的类型会有点不幸。上下文减少是一种将上述签名转换为也可以手写的签名或信息错误的方法。例如，由于一个人可能合理地拥有

instance Ord a => Ord (Tree a)

在范围内，我们可以将非法签名 Ord (Tree a) => ...进入法定签名 Ord a => ... .另一方面，如果我们没有 Eq 的任何实例对于范围内的函数，将报告关于类型的错误，该类型被推断为需要 Eq (a -> b)在其上下文中。

这还有其他几个好处:

直观的愉悦。许多上下文缩减规则不会改变类型是否合法，但确实反射(reflect)了人类在编写类型时会做的事情。我在这里考虑的是让你转向的重复数据删除和包含规则，例如(Eq a, Eq a, Ord a)进入 Ord a - 为了可读性，肯定会想要进行转换。

这可以经常捕获愚蠢的错误；而不是推断像 Eq (Integer -> Integer) => Bool 这样的类型中规中矩不能满足的，可以报Perhaps you did not apply a function to enough arguments?这样的错误.友好多了!

找出问题所在成为编译器的工作。而不是推断像 Eq (Tree (Grizwump a, [Flagle (Gr n e) (Gr n' e') c])) 这样的复杂上下文并提示上下文不可满足，而是被迫将其简化为构成约束；相反，它会提示我们无法确定 Eq (Grizwump a)从现有的上下文 - 一个更精确和可操作的错误。