Haskell中两个函数的最一般的“乘积”类型

Question

我必须从 Haskell 中的给定函数中找到最通用的类​​型，或者更确切地说，找到两个函数的“乘积”的最通用类型（如果存在）。我不确定，但也许我应该使用 Robinson 统一算法，但我无法理解。我需要一个详细的解决方案，一步一步来，这样我就明白了。

功能：

map :: (a → b) → [a] → [b] 
iterate :: (a → a) → a → [a]

如何找到最通用的类​​型

1. map iterate
2. iterate map

这不是家庭作业。

Answer 1

首先，明确写出所有省略的括号。

为了推导出a -> b 类型函数和c 类型值的应用类型，我们需要统一a 和c 类型，注意任何结果类型等价。那么应用程序的类型是b，在上述等价下。规则是：

f   ::     a → b
x   ::     c
        ----------
f x ::         b      , { a ~ c }

要半机械地找到这个，只需对齐类型并注意等价：

map ::    (   a1     →     b1     ) → ([a1] → [b1]) 
iterate :: (a2 → a2) → (a2 → [a2])
          --------------------------
        { a1 ~ (a2 → a2) , b1 ~ (a2 → [a2]) }

所以，

map iterate :: [a1] → [b1]

代入等价，我们得到

            :: [a2 → a2] -> [a2 → [a2]]

现在我们可以将 a2 重命名为 a 或 t 或其他任何名称。您的第二个示例类似：

iterate :: (   a2     →       a2     ) → (a2 → [a2])
map ::      (a1 → b1) → ([a1] → [b1]) 
           ---------------------------
        { a2 ~ a1 → b1 ,  a2 ~ [a1] → [b1] }

由于a2 ~ a2，我们得到a1 → b1 ~ [a1] → [b1]：

               a1  →  b1
              [a1] → [b1]
            --------------
        { a1 ~ [a1] ,  b1 ~ [b1] }

这两个等价都是不可能的，定义一个无限类型。所以第二个例子在 Haskell 中没有类型：

*Main> :t 映射迭代
地图迭代 :: [a -> a] -> [a -> [a]]

*Main> :t 迭代地图

:1:9:
发生检查：无法构造无限类型：a ~ [a]
预期类型：(a -> b) -> a -> b
实际类型：(a -> b) -> [a] -> [b]
在'iterate'的第一个参数中，即'map'
在表达式中：迭代地图

:1:9:
发生检查：无法构造无限类型：b ~ [b]
预期类型：(a -> b) -> a -> b
实际类型：(a -> b) -> [a] -> [b]
在'iterate'的第一个参数中，即'map'
在表达式中：迭代映射

Answer 2

让我们问 GHCi：

ghci> :type map . iterate
map . iterate :: (a -> a) -> [a] -> [[a]]
ghci> :type iterate . map
iterate . map :: (a -> a) -> [a] -> [[a]]

让我们看看它是如何得到它们的：

给定

map     :: (x -> y) -> [x] -> [y]
iterate :: (b -> b) -> b -> [b]
(.)     :: (s -> t) -> (r -> s) -> (r -> t)

并使用a ~ b 表示“a 和 b 类型相等”。

然后在map . iterate 我们有

map :: s -> t where
 s ~ x -> y
 t ~ [x] -> [y]

iterate :: r -> s where
 r ~ b -> b
 s ~ b -> [b]

so
 x -> y ~ s ~ b -> [b]
=>
 x ~ b
 y ~ [b]
 t ~ [b] -> [[b]]

所以map . iterate :: (b -> b) -> [b] -> [[b]]。

然后在iterate . map 我们有

iterate :: r -> s where
 s ~ b -> b
 t ~ b -> [b]

map :: s -> t where
 r ~ x -> y
 s ~ [x] -> [y]

so
 b -> b ~ s ~ [x] -> [y]
 b ~ [x]
 b ~ [y]
 x ~ y
 r ~ x -> x
 t ~ [x] -> [[x]]

所以iterate . map :: (x -> x) -> [x] -> [[x]]。

虽然这些函数具有相同的类型，但它们的行为却截然不同。

• iterate . map 将给定一个函数和一个长度为 k 的列表，生成一个长度为 k 的列表的无限列表。
• map . iterate 将给定一个函数和一个长度为k 的列表，生成一个长度为k 的无限列表。