haskell - 如何在 Morte 中输入 zipWith？

Question

这是 Morte 中几乎有效的 zipWith 定义:

zipWith
  =  λ (u : *)
  -> λ (f : (u -> u -> u))
  -> λ (a : (#List u))
  -> λ (b : (#List u))
  -> λ (List : *)
  -> λ (cons : (u -> List -> List))
  -> λ (nil : List)
  -> ((λ (A:*) -> λ (B:*) ->
  (a (B -> List)
    (λ (h:u) -> λ (t : (B -> List) -> λ k : B -> (k h t)))
    (λ (k:B) -> nil)
    (b (u -> A -> List)
      (λ (h:u) -> λ (t:(u -> A -> List)) -> λ (H:u) -> λ (k:A) -> (cons (f h H) (k t)))
      (λ (H:u) -> λ (k:A) -> nil)))
  ) (fix A . ((u -> A -> List) -> List))
    (fix B . (u -> (B -> List) -> List)))

由于使用了 fix，它实际上无法输入，而 Morte 缺乏这一点。 András posted this clever Agda solution without fix去年。但对我来说，它如何转化为 Morte 并不明显，因为它也缺乏归纳类型。如何解决这个问题？

编辑:即使使用fix，我的 zipWith 似乎也不正确。 This one不过，似乎要检查一下。

Answer 1

为了简单起见，我将使用常规 Haskell 列表。首先，让我们使用 foldr 定义 zipWith:

zipWith' :: (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' f xs ys = foldr step (const []) xs ys where
  step x r  []    = []
  step x r (y:ys) = f x y : r ys

在这里，我们折叠了xs，将ys作为参数传递，并在每次迭代时将其拆分。问题是我们想要模拟 Church 编码的列表，但它们不能进行模式匹配。然而，可以定义split

split :: [a] -> Maybe (a, [a])
split  []    = Nothing
split (x:xs) = Just (x, xs)

就foldr而言:

split :: [a] -> Maybe (a, [a])
split = snd . foldr (\x ~(r, _) -> (x : r, Just (x, r))) ([], Nothing)

现在我们可以仅使用正确的折叠来定义zipWith:

czipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
czipWith f xs ys = foldr step (const []) xs ys where
  step x r = maybe [] (\(y, ys) -> f x y : r ys) . split

然而，当 split 懒惰地遍历列表时(因此 split [1..] ≡ Just (1, [2..]))，它仍然会解构和重建整个列表，因此每个 split 都会引入 O(n) 开销，其中 n 是被拆分列表的长度。由于ys在每次迭代时都会被分割，因此算法的总复杂度为O(n^2)。

所以，是的，您可以仅使用非递归类型输入 zipWith，但时间复杂度为 O(n^2)。

<小时/>

此外，消除器是依赖的​​同态，而同态确实可以为您提供模式匹配，因此如果您有消除器，则它是 straightforward定义 O(n) zipWith 并且它不必像您链接的 András' 答案中那样复杂。

一些阅读:

• 在键入设置中，Church 编码称为 Boehm-Berarducci编码。
• How to zip folds .
• How to take a TAIL of a functional stream .
• 我使用的 foldr 中 split 的定义在 TAPL 中的某处进行了描述。 .