了解 foldTree 函数的类型推导

Question

查看 Data.Tree 中出现的这个定义：

foldTree :: (a -> [b] -> b) -> Tree a -> b
foldTree f = go where
    go (Node x ts) = f x (map go ts)

我的具体问题是：由于go名字出现在(map go ts)等式的右边，函数的类型如何

(a -> [b] -> b)

正在推断？

例如有这行代码：

foldTree (:) (Node 1 [Node 2 []])

实例化定义：

foldTree (:) = go where
    go (Node 1 [Node 2 []]) = (:) 1 (map go [Node 2 []])

(:) 1 (map go [Node 2 []]) 未完全评估，所以我只看到 (:) 1 具有类型 Num a => [a] -> [a]。但是，缺少一个间隙，为了填补它，应该完成递归。因此，计算类型似乎有些循环。

非常感谢任何见解。

Answer 1

Haskell的类型推断很巧妙！我无法告诉你这实际上是如何推断出来的，但让我们来看看它是如何推断出来的。现实可能离我们不远了。在这种情况下实际上不需要类型签名。

foldTree f = go where
    go (Node x ts) = f x (map go ts)

foldTree 被定义为带参数，go 被定义为带参数，所以我们从一开始就知道它们是函数。

foldTree :: _a -> _b
foldTree f = go where
    go :: _c -> _d
    go (Node x ts) = f x (map go ts)

现在我们看到 f 是用两个参数调用的，所以它实际上必须是（至少）两个参数的函数。

foldTree :: (_x -> _y -> _z) -> _b
foldTree f = go where
    go :: _c -> _d
    go (Node x ts) = f x (map go ts)

由于 foldTree f = go 和 go :: _c -> _d，结果类型 _b 实际上必须是 _c -> _d *:

foldTree :: (_x -> _y -> _z) -> _c -> _d
foldTree f = go where
    go :: _c -> _d
    go (Node x ts) = f x (map go ts)

传递给 f 的第二个参数（_y 类型）是 map go ts。由于 go :: _c -> _d，_y 必须是 [_d]

foldTree :: (_x -> [_d] -> _z) -> _c -> _d
foldTree f = go where
    go :: _c -> _d
    go (Node x ts) = f x (map go ts)

go 将其参数与 Node x ts 相匹配，而 Node 是 Tree 的数据构造函数，因此 go 的参数（_c) 必须是 Tree.

foldTree :: (_x -> [_d] -> _z) -> Tree _p -> _d
foldTree f = go where
    go :: Tree _p -> _d
    go (Node x ts) = f x (map go ts)

Node构造函数的第一个字段作为f的第一个参数传递，所以_x和_p必须相同：

foldTree :: (_x -> [_d] -> _z) -> Tree _x -> _d
foldTree f = go where
    go :: Tree _x -> _d
    go (Node x ts) = f x (map go ts)

由于go _被定义为f _ _，它们必须有相同类型的结果，所以_z是_d:

foldTree :: (_x -> [_d] -> _d) -> Tree _x -> _d
foldTree f = go where
    go :: Tree _x -> _d
    go (Node x ts) = f x (map go ts)

哇哦。现在，编译器会检查以确保这些类型可以解决（它们确实可以解决），并将它们从“元变量”（意味着推理引擎不知道它们代表什么类型的变量）“概括”为量化类型变量（变量绝对是多态的），它得到

foldTree :: forall a b. (a -> [b] -> b) -> Tree a -> b
foldTree f = go where
    go :: Tree a -> b
    go (Node x ts) = f x (map go ts)

实际情况有点复杂，但这应该给了你要点。

[*] 这一步有点作弊。我忽略了一个叫做“let generalization”的特性，在这个上下文中不需要它，实际上它被 GHC 中的几种语言扩展禁用 Haskell.

Answer 2

这是针对此问题的类型推导展开sheet。把所有的东西都放在一起会更容易理解：

data Tree a = Node a [Tree a]

foldTree f = go  where
  go (Node x ts) = f x (map go ts)

foldTree f t = go t  where
  go t@(Node x ts) = f x (map go ts)
--------------------------------------
     Tree a                                  t  :: Tree a       from `data Tree a`
             a         a                     x  :: a            from `data Tree a`
              [Tree a]           [Tree a]    ts :: [Tree a]     from `data Tree a`
                              Tree a -> b    go :: Tree a -> b  from type of `map`
                          [b]                                   from type of `map`
               f  :: a -> [b] -> r                some resulting type `r`
               go :: Tree a   -> r                from definition of `go`
               go :: Tree a   -> b                as derived above
                     ----------------------
                               r ~ b              `r` and `b` are the same type
                     ----------------------
               f  :: a -> [b] ->   b              more precise type now
             ------------------------------
foldTree :: (a -> [b] -> b) -> Tree a -> b
foldTree    f               =  go

这里我们从 t 的类型开始，但无论起点如何，派生类型都将始终相同，直到对其类型变量进行一致的重命名。

这个符号的解释：我们从上到下，从左到右阅读这个。我试图以暗示的方式对齐相关的东西垂直。想象一下，你用它的类型注释每个实体，用较小的字母和不同的颜色（比如，红色）在纸上的 sheet 上写下那个实体附近的类型，上面有所有代码（写成蓝色，比如写成蓝色）。相反，在这里，我们将类型写在该实体下，垂直对齐（即使它们之间还有一些其他行）。

比如推导部分第二行在x下面写了两个a，旁边还有一些注释。这是什么意思？

每个a都写在一个x下。就像我们已经用类型 a 注释了每个 x。由于 x 在两个实例中都是相同的 x，因此类型是相同的类型。我们还不太了解它，所以我们就称它为 a —— 一个类型变量，如果它在推理过程中进一步发生的话，能够在以后采用另一个更精确的含义。然后，有一个旁注：x :: a 是一个常规的 Haskell 表示法，这意味着 x 的类型为 a。所以它说的是同样的事情，但更正式。然后有一个非正式的说明，说明这个决定从何而来。

了解 foldTree 函数的类型推导

Understanding foldTree function's type derivation

haskell

types

tree

type-inference

fold