“折叠地图”的类型.折叠地图'

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和(.)的类型派生该类型？我特别困惑的是，在foldMap的类型中找不到的"新"类型t (t1 a)如何出现在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的平等内部。 我们知道，对于某些b，foldMap₂ . foldMap₁的结果类型将是t b -> m;碰巧的是，统一foldMap₁的输出和foldMap₂的输入会限制b成为s a类型。 我们总是可以将类型变量与更复杂的类型表达式统一起来（只要更复杂的表达式不涉及原始类型变量; b和t b将无法统一），这有时会导致有趣的类型，例如t (s a)当它发生在幕后时。

Answer 2

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

也可以看作是

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

因为->与右边有关。插入到定义中

(.) :: (y -> z) -> (x -> y) -> (x -> z)

我们明白了

x = (Monoid m) => a -> m
y = (Foldable ty, Monoid m) => ty a -> m

在这里，您必须将a替换为foldMap中的ty a：

z = (Foldable ty, Foldable tz, Monoid m) => tz (ty a) -> m

你从(.)中得到的是

x -> z

这只是另一种说法

(Foldable ty, Foldable tz, Monoid m) => (a -> m) -> (tz (ty a) -> m)

当删除不必要的括号时，它是

(Foldable ty, Foldable tz, Monoid m) => (a -> m) -> tz (ty a) -> m

或者——正如ghci所写的——

(Foldable t, Foldable t1, Monoid m) => (a -> m) -> t (t1 a) -> m

Answer 3

暂时省略 typeclass 约束，可以写出 foldMap 和 (.) 的签名：

foldMap :: (a -> m) -> (t a -> m)
    (.) :: (y -> z) -> (x -> y) -> (x -> z) -- this is just a change of variables

在这里，我们使用了函数应用程序与右侧关联的事实。

因此，分析foldMap . foldMap的类型签名会建立以下对应关系：

      foldMap          .              foldMap
(a -> m) -> (t a -> m)   ( a' -> m') -> (t' a' -> m')    (a' -> m') -> (t a -> m)
  (y     ->    z)     ->        (x   ->   y)          ->     (x     ->    z)

即我们有以下类型等式：

y = a -> m
z = t a -> m
x = a' -> m'
y = t' a' -> m'
x = a' -> m'
z = t a -> m

这简化为：

a = t' a'
m = m'

即foldMap . foldMap的类型是(a' -> m) -> (t (t' a') -> m)或等效(a' -> m) -> t (t' a) -> m.