在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. 

Answer 1

这是关于数据声明的上下文的众所周知的问题.如果你定义data Ord a => Tree a = ...它所做的就是强制任何提到Tree a有Ord a上下文的函数.这并没有为您节省任何打字,但从正面来看,明确的背景清楚地表明需要什么.

GADTs救援!

解决方法是使用广义抽象数据类型(GADTs).

{-# Language GADTs, GADTSyntax #-}

我们可以通过提供一个explict类型签名直接将上下文放在构造函数上:

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

一切正常.哇是因为隐式Eq a上下文意味着我们不需要Eq a在实例上显式.

上下文仅来自contstructors

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

这实际上是我们需要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

你会得到一个no instance for (Ord a)错误,因为左侧没有构造函数来给你(Ord a,Eq a)上下文.

这意味着你仍然需要

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

这次没有办法绕过它,对不起,但从好的方面来看,这可能是你想要写的唯一没有树参数的树函数.大多数树函数将在定义的左侧使用树,并对其做一些事情,因此大多数时候您将拥有隐式上下文.