如何在Morte中输入zipWith？

Question

这是zipWithMorte中几乎有效的定义:

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)))

由于使用fixMorte缺乏,它实际上不是可打字的.Andrásfix去年发布了这款聪明的Agda解决方案.然而,对我而言,它如何转化为Morte并不明显,因为它也缺乏归纳类型.如何解决这个问题？

编辑:看起来我的zipWith甚至不正确fix.但是,这个似乎在检查.

Answer 1

为简单起见,我将使用常规的Haskell列表.首先,让我们定义zipWith使用foldr:

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作为参数传递并在每次迭代时拆分它.问题是我们想要模仿教会编码的列表,但它们不能模式匹配.但是可以定义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懒惰地遍历列表(so split [1..] ? Just (1, [2..])),但它仍然解构并重构整个列表,因此每个都split引入了O(n)开销,其中n列表的长度被分割.由于ys在每次迭代时分裂,因此算法的总复杂度为O(n ^ 2).

所以是的,您可以zipWith只使用非递归类型键入,但它将是O(n ^ 2).

此外,除水都依赖paramorphisms和paramorphisms给你做模式匹配,所以如果你有消除器,它是简单的定义为O(n) zipWith ,它并没有成为复杂,因为在安德拉什的回答您联系.

一些阅读:

• 在类型设置中,Church编码称为Boehm-Berarducci编码.
• 如何拉链折叠.
• 如何获取功能流的TAIL.
• 的这个定义split来讲foldr,我用在什么地方描述TAPL.