haskell - `foldMap . foldMap` 的类型

Question

(这是 Typeclassopedia 中的练习。)

如何计算两个非平凡函数的组合类型，例如 foldMap . foldMap ?

对于简单的情况，这很容易:只需查看 (.) 的类型即可。

(.) :: (b -> c) -> (a -> b) -> (a -> c)

并找到类型 a , b和 c对于这两个函数。

在 foldMap的情况下，类型是

foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m

我认为没有办法将这个函数的类型“拆分”成两部分，这样我就可以得到“a”、“b”和“c”，就像 (.) 的类型一样。 .

然后我问 ghci来计算它的类型。它成功了以下类型:

Prelude Data.Foldable> :t foldMap . foldMap 
foldMap . foldMap
  :: (Foldable t, Foldable t1, Data.Monoid.Monoid m) =>
     (a -> m) -> t (t1 a) -> m

我如何从 foldMap 派生该类型和 (.)的类型？我特别困惑"new"类型 t (t1 a)在 foldMap 中找不到的类型可以显示在 foldMap . foldMap 的类型中.

Answer 1

在简单情况下工作的相同等式推理技术将在这个更复杂的情况下继续工作。要记住的一件重要的事情是 -> 是右结合的；这意味着 a -> b -> c 与 a -> (b -> c) 相同；因此，Haskell 中的所有函数只接受一个输入并产生一个输出，因此可以组合。 (这种等价性是在任何地方进行部分应用的能力背后的原因。)因此，我们可以将 foldMap 的类型签名重写为

foldMap :: (Foldable t, Monoid m) => (a -> m) -> (t a -> m)

为清楚起见，我将为 foldMap 的两个不同出现提供不同的名称，并为其类型变量使用不同的名称；我们将有 foldMap₂ . foldMap₁ ，其中

foldMap₁ :: (Foldable s, Monoid n) => (a -> n) -> (s a -> n)
foldMap₂ :: (Foldable t, Monoid m) => (b -> m) -> (t b -> m)
(.)      :: (d -> e) -> (c -> d) -> (c -> e)

因此，情况一定是

foldMap₂ . foldMap₁ :: c -> e

但是 c 和 e 是什么，允许它工作的 d 是什么？离开类约束(它们只是在最后结合在一起，一路上会把一切都弄乱)，我们知道

                                            foldMap₂ . foldMap₁ ---+
                                                                   |
                                                                   |
       /-------foldMap₂-------\    /-------foldMap₁-------\    /---+--\
(.) :: (d        -> e         ) -> (c        -> d         ) -> (c -> e)
       ((b -> m) -> (t b -> m)) -> ((a -> n) -> (s a -> n))

这产生了以下等式(请记住，Haskell 拼写了类型等式 ~):

(c -> d) ~ ((a -> n) -> (s a -> n))
(d -> e) ~ ((b -> m) -> (t b -> m))

因为这些是函数类型的相等，我们知道域和范围分别彼此相等:

c ~ (a -> n)
e ~ (t b -> m)
d ~ (b -> m)
d ~ (s a -> n)

我们可以折叠 d 等式，通过传递性得出结论，即

(b -> m) ~ (s a -> n)

然后，由于双方都是函数类型，我们可以分解这种等式得出结论:

b ~ s a
m ~ n

所以 d ~ (s a -> n) ，或者换句话说只是 foldMap₁ 的结果类型——诀窍是 b -> m ， foldMap₂ 的输入类型，足够通用，可以与前一种类型统一! (在这里，统一是类型推断器所做的；如果将更具体的类型替换为类型变量时，两种类型可以相同，则它们可以统一。)

最后，然后，代入 c 和 e ，我们得到

(c -> e) ~ ((a -> n) -> e)                 by the equality for c
         ~ ((a -> n) -> (t b -> m))        by the equality for e
         ~ ((a -> m) -> (t b -> m))        by the equality for n
         ~ ((a -> m) -> (t (s a) -> m))    by the equality for b

因此，当我们添加回完整的类约束列表(记住 Monoid m 和 Monoid n 实际上是相同的约束，因为 m ~ n )并删除冗余的括号对，我们得到

foldMap . foldMap :: (Foldable s, Foldable t, Monoid m)
                  => (a -> m) -> t (s a) -> m

在重命名之前，这与 GHCi 给您的相同。

请特别注意最后一步，其中出现了嵌套类型 t (s a)。这来自上面 b 的统一，在关于 d 的等式内部。我们知道，对于某些 foldMap₂ . foldMap₁ ， t b -> m 的结果类型将是 b ；碰巧统一 foldMap₁ 的输出和 foldMap₂ 的输入将 b 限制为类型 s a 。我们总是可以用更复杂的类型表达式来统一类型变量(只要更复杂的表达式不涉及原始类型变量； b 和 t b 将无法统一)，这有时会导致像 t (s a) 这样有趣的类型，当它发生在后面时场景。