Haskell中用于自动函数约束推导的类型约束

Question

出于教育目的，我正在使用Haskell玩弄树。 我定义了像这样的Tree a类型

data Tree a = EmptyTree | Node a (Tree a) (Tree a)

许多函数都有一个共同的基本约束条件 - Ord a，因此它们的类型看起来像：

treeInsert :: Ord a => a -> Tree a -> Tree a
treeMake :: Ord a => [a] -> Tree a

等等，我也可以像这样定义Tree a

data Ord a => Tree a = EmptyTree | Node a (Tree a) (Tree a)

但我无法简化我的函数并省略额外的 Ord a，使其如下所示：

treeInsert :: a -> Tree a -> Tree a
treeMake :: [a] -> Tree a

为什么 Haskell（使用 -XDatatypeContexts）不能自动推断这个约束？我认为它应该很明显。我错了吗？

下面是一些示例源代码：

data (Eq a, Ord a) => Tree a = EmptyTree | Node a (Tree a) (Tree a)

treeInsert :: a -> Tree a -> Tree a
treeInsert a EmptyTree = Node a EmptyTree EmptyTree
treeInsert a node@(Node v left right)
 | a == v = node
 | a > v = Node v left (treeInsert a right)
 | a < v = Node v (treeInsert a left) right

mkTree :: [a] -> Tree a
mkTree [] = EmptyTree
mkTree (x:xs) = treeInsert x (mkTree xs)

我遇到了这个问题

Tree.hs:5:26:
    No instance for (Ord a)
      arising from a use of `Node'
    In the expression: Node a EmptyTree EmptyTree
    In an equation for `treeInsert':
        treeInsert a EmptyTree = Node a EmptyTree EmptyTree
Failed, modules loaded: none. 

- tomas789

---

为什么最新版的GHC已经弃用了DataTypeContexts？这篇文章似乎与此相关。 - raymonad

raymonad的链接包含了你要找的内容。GADT风格的声明在一个重要方面有所不同：它们以不同的方式处理数据构造函数上的类约束。具体来说，如果构造函数给定了类型类上下文，则该上下文可通过模式匹配获得。 - phipsgabler

在上下文中，Eq和Ord都是不必要的。Eq是Ord的超类，因此后者已经足够了。 - augustss

Answer 1

这是一个关于数据声明上下文的众所周知的陷阱。如果你定义 data Ord a => Tree a = ...，那么它只会强制任何提到 Tree a 的函数都需要一个 Ord a 上下文。这并不能为你节省打字时间，但好处在于明确指出了需要什么样的上下文。

GADTs能够解决这个问题！使用广义代数数据类型（GADTs）可以规避这个问题。

{-# Language GADTs, GADTSyntax #-}

我们可以通过提供显式的类型签名，在构造函数上直接设置上下文：

data Tree a where
   EmptyTree :: (Ord a,Eq a) => Tree a
   Node :: (Ord a,Eq a) => a -> Tree a -> Tree a -> Tree a

每当我们使用 Node a left right 进行模式匹配时，就会隐含地得到 (Ord a,Eq a) 上下文，正如您所希望的那样，因此我们可以从这里开始定义 treeInsert，代码如下：

treeInsert :: a -> Tree a -> Tree a
treeInsert a EmptyTree = Node a EmptyTree EmptyTree
treeInsert a (Node top left right) 
          | a < top   = Node top (treeInsert a left) right
          | otherwise = Node top left (treeInsert a right) 

派生

如果你只是添加deriving Show，那么会出现错误：

Can't make a derived instance of `Show (Tree a)':
  Constructor `EmptyTree' must have a Haskell-98 type
  Constructor `Node' must have a Haskell-98 type
  Possible fix: use a standalone deriving declaration instead
In the data type declaration for `Tree'

虽然有点麻烦，但是像它所说的那样，如果我们添加了 StandaloneDeriving 扩展 ({-# Language GADTs, GADTSyntax, StandaloneDeriving #-})，我们就可以做一些类似于以下的事情：

deriving instance Show a => Show (Tree a)
deriving instance Eq (Tree a) -- wow

一切都顺利。"Wow"的原因是因为隐式的Eq a上下文意味着我们不需要在实例中显式地使用Eq a。

上下文只来自构造函数

请记住，您只能从使用其中一个构造函数中获得隐式上下文。(记住这是上下文定义的位置。)

这实际上就是为什么我们需要在EmptyTree构造函数中使用上下文的原因。如果我们只是使用了EmptyTree::Tree a，那么这行代码：

treeInsert a EmptyTree = Node a EmptyTree EmptyTree

左侧的等式不应该有 (Ord a,Eq a) 的限制条件，否则实例将会缺失在右侧，在Node构造函数中需要这些实例。如果出现这种情况，就会产生错误，因此在这种情况下保持上下文的一致性是很有帮助的。

这也意味着您不能有

treeMake :: [a] -> Tree a

treeMake xs = foldr treeInsert EmptyTree xs

如果左侧没有构造函数为您提供(Ord a, Eq a)上下文，那么您将会遇到no instance for (Ord a)错误。

这意味着您仍然需要

treeMake :: Ord a => [a] -> Tree a

很抱歉，这一次必须要用树形结构，但好处是，这可能是您在没有树形参数的情况下想要编写的唯一树函数。大多数树函数将在定义左侧接收一个树形参数，并对其进行某些操作，因此您将大部分时间具有隐含的上下文。

- AndrewC

---

@Satvik，它在mkTree上不起作用，因为左侧没有Tree a构造函数，所以您不会得到隐式上下文，这仅来自构造函数。这是一个很好的观点，所以我会编辑一些关于它的内容，谢谢。 - AndrewC

@Satvik 完成 - 最后一节解释清楚了吗？ - AndrewC

是的，它解释得很好。 - Satvik

绝对完美而详尽的回答。谢谢！ - tomas789

@tomas789：详尽的回答通常会让人感到疲惫不堪。 - Claudiu

Answer 2

kirelagin关于DatatypeContexts无用的说法是正确的。你仍然需要在所有函数中编写类约束。但如果你有很多类，这里有一个小技巧，可以让你只使用一个类。

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

data Tree a = EmptyTree | Node a (Tree a) (Tree a) deriving Show

class (Eq a, Ord a) => Foo a where

instance (Eq a, Ord a) => Foo a where

treeInsert :: Foo a => a -> Tree a -> Tree a
treeInsert a EmptyTree = Node a EmptyTree EmptyTree
treeInsert a node@(Node v left right)
 | a == v = node
 | a > v = Node v left (treeInsert a right)
 | a < v = Node v (treeInsert a left) right

mkTree :: Foo a => [a] -> Tree a
mkTree [] = EmptyTree
mkTree (x:xs) = treeInsert x (mkTree xs)

现在 Foo 类似于 Eq && Ord。使用类似的例子，您可以在所有函数中只用一个类替换掉所有的类。正如 @luqui 所指出的那样，您也可以使用 ConstraintKinds 使其工作。

或者您可以使用我认为允许您在数据定义中提到类约束的 GADTs。

- Satvik

---

使用ConstraintKinds，可以简单地定义类型为type Foo a = (Eq a, Ord a)。这意味着类型a必须同时满足相等性和可排序性的约束条件。 - luqui

@AndrewC 感谢您指出这一点。问题在于你不能完全避免所有函数中的上下文（例如mkTree的示例）。已经有一个回答指向了如何使用GADTs来实现类似的东西。我只是想指出一种简化上下文的方法，当有许多类在所有函数中重复时。 - Satvik

Errm Eq 是 Ord 的一个超类。如果你写成 :: Ord a => ...，那么你就可以免费获得 Eq a。 - AntC

Answer 3

问题在于这个约束只适用于构造函数，而不是整个数据类型。这就是为什么 DatatypeContexts 实际上几乎没有用处... 你可以在 这里 阅读更多相关信息。

如果你希望第二段包含解决方案，那么很遗憾，我不知道这样的解决方案，并且似乎确实 不存在。维基百科文章提到了使用 MultiParamTypeClasses 的方法，但老实说，那并不方便。

- kirelagin

---

我已更新了那个维基页面，就像一段时间前我所建议的那样。 - AndrewC

我完全同意“说实话不太方便”这个关于多参数类型类的观点。 - AndrewC