为什么需要减少上下文？

Question

我刚读过这篇论文("类型类:Peyton Jones&Jones对设计空间的探索"),它解释了Haskell早期类型类系统的一些挑战,以及如何改进它.

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

例如,如果你在某个地方,instance (Ord a, Ord b) => Ord (a, b) ...那么在上下文中,Ord (a, b)减少到{Ord a, Ord b}(减少并不总是缩小约束的数量).

我不明白为什么这种减少是必要的.

好吧,我收集它用于执行某种形式的类型检查.当你有一组简化的约束时,你可以检查是否存在一些可以满足它们的实例,否则就是一个错误.我不太确定它的附加价值是什么,因为你会注意到使用网站上的问题,但没关系.

但即使您必须进行检查,为什么要在推断类型中使用缩减结果？该文指出它导致了不直观的推断类型.

这篇论文非常古老(1997),但就我所知,背景减少仍然是一个持续关注的问题.Haskell 2010规范确实提到了我在上面解释的推理行为(链接).

那么,为什么这样呢？

Answer 1

我不知道这是否是The Reason,但是它可能被认为是一个原因:在早期的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在范围内没有for函数的任何实例,则会报告有关Eq (a -> b)在其上下文中推断为需要的类型的错误.

这还有其他一些好处:

1. 直觉上令人愉悦.许多上下文缩减规则不会改变类型是否合法,但确实反映了人类在编写类型时会做的事情.我在想,让你转,例如重复数据删除和包容的规则在这里(Eq a, Eq a, Ord a)逼到Ord a-转换一个铁定要为可读性做.
2. 这经常会发现愚蠢的错误; Eq (Integer -> Integer) => Bool人们可以报告错误,而不是推断出一种不能以一种守法的方式满足的类型Perhaps you did not apply a function to enough arguments?.更友好!
3. 编译器的工作就是找出出错的地方.而不是推断复杂的上下文,Eq (Tree (Grizwump a, [Flagle (Gr n e) (Gr n' e') c]))并抱怨上下文不可满足,而是被迫将其减少到组成约束; 相反,它会抱怨我们无法Eq (Grizwump a)从现有的背景中确定- 更精确和可操作的错误.

Answer 2

我认为这在传递实现的字典中确实是可取的.在这样的实现中,"字典",即元组或函数记录被作为所应用函数的类型中的每个类型类约束的隐式参数传递.

现在,问题是这些词典的创建时间和方式.观察对于简单类型,例如Int必要时,任何类型类的所有字典Int都是一个常量的实例.在列表Maybe或元组等参数化类型的情况下不是这样.很明显,为了显示元组,例如,Show需要知道实际元组元素的实例.因此,这样的多态字典不能是常数.

似乎指导字典传递的原则是这样的:只传递在所应用函数的类型中作为类型变量出现的类型的字典.或者,换句话说:没有复制冗余信息.

考虑这个功能:

 f :: (Show a, Show b) => (a,b) -> Int
 f ab = length (show ab)

可显示组件的元组也可显示的信息,因此Show (a,b)当我们已经知道时,不需要出现约束(Show a, Show b).

但是,另一种实现方式是可能的,其中调用者将负责创建和传递字典.这可以在没有上下文减少的情况下工作,这样的类型f看起来像:

f :: Show (a,b) => (a,b) -> Int

但这意味着创建元组字典的代码必须在每个调用站点上重复.并且很容易得出必要约束数量实际增加的示例,例如:

g :: (Show (a,a), Show(b,b), Show (a,b), Show (b, a)) => a -> b -> Int
g a b = maximum (map length [show (a,a), show (a,b), show (b,a), show(b,b)])

使用显式传递的实际记录实现类型类/实例系统是有益的.例如:

data Show' a = Show' { show' :: a -> String }
showInt :: Show' Int
showInt = Show' { show' = intshow } where
      intshow :: Int -> String
      intshow = show

一旦这样做,您可能很容易认识到"减少上下文"的必要性.