为什么 Haskell 不接受我的组合“zip”定义？

Question

这是教科书的zip功能：

zip :: [a] -> [a] -> [(a,a)]
zip [] _ = []
zip _ [] = []
zip (x:xs) (y:ys) = (x,y) : zip xs ys

我早些时候在#haskell 上询问过“zip”是否可以单独使用“foldr”来实现，没有递归，没有模式匹配。经过一番思考，我们注意到可以使用延续来消除递归：

zip' :: [a] -> [a] -> [(a,a)]
zip' = foldr cons nil
    where
        cons h t (y:ys) = (h,y) : (t ys)
        cons h t []     = []
        nil             = const []

我们还剩下模式匹配。经过更多的神经元敬酒后，我想出了一个我认为合乎逻辑的不完整答案：

zip :: [a] -> [a] -> [a]
zip a b = (zipper a) (zipper b) where
    zipper = foldr (\ x xs cont -> x : cont xs) (const [])

它返回一个平面列表，但会进行压缩。我确信这是有道理的，但 Haskell 抱怨这种类型。我继续在一个无类型的 lambda 计算器上对其进行测试，它工作正常。为什么 Haskell 不能接受我的函数？

错误是：

zip.hs:17:19:
    Occurs check: cannot construct the infinite type:
      t0 ~ (t0 -> [a]) -> [a]
    Expected type: a -> ((t0 -> [a]) -> [a]) -> (t0 -> [a]) -> [a]
      Actual type: a
                   -> ((t0 -> [a]) -> [a]) -> (((t0 -> [a]) -> [a]) -> [a]) -> [a]
    Relevant bindings include
      b ∷ [a] (bound at zip.hs:17:7)
      a ∷ [a] (bound at zip.hs:17:5)
      zip ∷ [a] -> [a] -> [a] (bound at zip.hs:17:1)
    In the first argument of ‘foldr’, namely ‘cons’
    In the expression: ((foldr cons nil a) (foldr cons nil b))

zip.hs:17:38:
    Occurs check: cannot construct the infinite type:
      t0 ~ (t0 -> [a]) -> [a]
    Expected type: a -> (t0 -> [a]) -> t0 -> [a]
      Actual type: a -> (t0 -> [a]) -> ((t0 -> [a]) -> [a]) -> [a]
    Relevant bindings include
      b ∷ [a] (bound at zip.hs:17:7)
      a ∷ [a] (bound at zip.hs:17:5)
      zip ∷ [a] -> [a] -> [a] (bound at zip.hs:17:1)
    In the first argument of ‘foldr’, namely ‘cons’
    In the fourth argument of ‘foldr’, namely ‘(foldr cons nil b)’

Answer 1

至于你的定义为什么不被接受：看看这个：

λ> :t \ x xs cont -> x : cont xs
 ... :: a -> r -> ((r -> [a]) -> [a])

λ> :t foldr
foldr :: (a' -> b' -> b') -> b' -> [a'] -> b'

所以如果你想使用第一个函数作为foldr 的参数，你会得到（如果你匹配foldrs 第一个参数的类型：

a' := a
b' := r
b' := (r -> [a]) -> [a]

这当然是个问题（r 和 (r -> [a]) -> [a] 相互递归，应该都等于 b'）

这是编译器告诉你的

如何修复它

您可以使用

修复您的想法

newtype Fix a t = Fix { unFix :: Fix a t -> [a] }

这是我借来的original use。

你可以这样写：

zipCat :: [a] -> [a] -> [a]
zipCat a b = (unFix $ zipper a) (zipper b) where
  zipper = foldr foldF (Fix $ const [])
  foldF x xs = Fix (\ cont -> x : (unFix cont $ xs))

你会得到：

λ> zipCat [1..4] [5..8]
[1,5,2,6,3,7,4,8]

这是（我认为的）你想要的。

但是很明显，您的两个列表都需要属于同一类型，所以我不知道这是否真的对您有帮助

Answer 2

我可以为您提供一个稍微不同的视角（我认为），以得出与 Carsten 类似的解决方案（但类型更简单）。

这是你的代码，你的“编织拉链”（我写tr代表“r的类型”，同样tq代表“q的类型”；我总是使用“ r" 用于foldr 定义中组合函数的递归结果 参数，作为助记符）：

zipw :: [a] -> [a] -> [a]
zipw xs ys = (zipper xs) (zipper ys) where
    zipper xs q = foldr (\ x r q -> x : q r) (const []) xs q
                        --- c -------------- --- n ----

 -- zipper [x1,x2,x3] (zipper ys) =
 -- c x1 (c x2 (c x3 n)) (zipper ys)
         --- r --------  --- q -----  tr ~ tq ; q r :: [a]
                                      --     => r r :: [a]
                                      -- => r :: tr -> [a] 
                                      --   tr ~  tr -> [a]    

所以，这是无限类型。 Haskell 不允许这用于任意类型（这是类型变量所代表的）。

但 Haskell 的数据类型确实承认递归。列表、树等——所有常见的类型都是递归的。这是允许的：

data Tree a = Branch (Tree a) (Tree a)

这里我们确实在等式的两边都有相同的类型，就像我们在类型等价的两边都有tr，tr ~ tr -> [a]。但它是一种特定类型，而不是任意类型。

所以我们只是这样声明它，遵循上面的“等式”：

newtype TR a = Pack { unpack :: TR a -> [a] } 
           -- unpack :: TR a -> TR a -> [a]

什么是Tree a 类型？这是进入Branch 的“东西”，即Tree a。给定的树不必无限构造，因为undefined 也有类型Tree a。

什么是TR a 类型？这是进入TR a -> [a] 的“东西”，即TR a。给定的TR a 不必无限构造，因为const [] 也可以是TR a 类型。

我们想要的递归类型tr ~ tr -> [a] 已成为真正的递归类型定义newtype TR a = Pack { TR a -> [a] }，隐藏在数据构造函数Pack 后面（由于使用了newtype 关键字，编译器将删除它，但这是一个无关紧要的细节；它也适用于data）。

Haskell 在这里为我们处理递归。类型理论家喜欢自己处理这个问题，Fix 等等；但是 Haskell 用户已经可以使用该语言。我们不必了解它是如何实现的，就可以使用它。在我们想自己建造之前，无需重新发明轮子。

所以，zipper xs 的类型为 tr；现在它变成了TR a，所以这就是新的zipper xs 必须返回的——“打包”列表生成函数。 foldr 组合函数必须返回 zipper 调用返回的内容（根据 foldr 定义的优点）。要应用打包函数，我们现在需要先unpack：

zipw :: [a] -> [a] -> [a]
zipw xs ys = unpack (zipper xs) (zipper ys)
    where
    zipper :: [a] -> TR a
    zipper = foldr (\ x r -> Pack $ \q -> x : unpack q r)
                   (Pack $ const [])

Answer 3

我们可以通过定义一个为我们执行此操作的函数来消除显式模式匹配。

这是作弊吗？如果maybe 和bool 被允许，则不是这样；那么我们也应该允许list（也在extra的Data.List.Extra中），

list :: b -> (a -> [a] -> b) -> [a] -> b 
list n c []     = n
list n c (x:xs) = c x xs

也一样；这样我们就可以在您的zip' 定义中拥有，

cons h t = list [] (\y ys -> (h,y) : t ys)

或例如

         = list [] (uncurry ((:).(h,).fst <*> t.snd))
         = list [] (curry $ uncurry (:) . ((h,) *** t))
         = list [] (flip ((.) . (:) . (h,)) t)
         = list [] ((. t) . (:) . (h,))

如果你喜欢这种东西。

关于你的错误，“无限类型”通常表示自我应用；事实上，无论你的 zipper 返回什么，你都在自己应用它，在你的

zip a b = (zipper a) (zipper b)  where ....

---

我试图调整你的定义并想出了

zipp :: [a] -> [b] -> [(a,b)]
zipp xs ys = zip1 xs (zip2 ys)
  where
     -- zip1 :: [a] -> tq -> [(a,b)]          -- zip1 xs :: tr ~ tq -> [(a,b)]
     zip1 xs q = foldr (\ x r q -> q x r ) n xs q 
                       -------- c --------
     n    q  = []

     -- zip2 :: [b] -> a -> tr -> [(a,b)]     -- zip2 ys :: tq ~ a -> tr -> [(a,b)]
     zip2 ys x r = foldr (\ y q x r -> (x,y) : r q ) m ys x r  
                         ---------- k --------------
     m  x r  = []

{-
  zipp [x1,x2,x3] [y1,y2,y3,y4]

= c x1 (c x2 (c xn n)) (k y1 (k y2 (k y3 (k y4 m))))
       ---------------       ----------------------
        r                     q

= k y1 (k y2 (k y3 (k y4 m))) x1 (c x2 (c xn n))
       ----------------------    ---------------
        q                         r
-}

它似乎在纸上正确地减少了，但我在这里也遇到了无限的类型错误。

现在没有（立即明显的）自我应用，但是第一个 zip 获得的延续类型取决于第一个 zip 本身的类型；所以仍然存在循环依赖：tq 在tq ~ a -> tr -> [(a,b)] ~ a -> (tq -> [(a,b)]) -> [(a,b)] 中的类型等价的两侧。

确实这是我得到的两个类型错误，（第一个是关于 tr 类型的），

Occurs check: cannot construct the infinite type:
  t1 ~ (a -> t1 -> [(a, b)]) -> [(a, b)]          -- tr

Occurs check: cannot construct the infinite type:
  t0 ~ a -> (t0 -> [(a, b)]) -> [(a, b)]          -- tq

在使用foldr 和延续的通常定义中，这些延续的类型是独立的；我猜这就是它在那里工作的原因。

• 也可以在这里查看我的second answer 和this follow-up Q&A