仅使用 foldr 定义 zip 时出现无限类型错误；可以修复吗？

Question

（有关此内容的上下文，请参阅）。

我试图仅使用 foldr 得出 zip 的定义：

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

它在纸面上 "works"，但给出了两个 "infinite type" 错误：

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

显然，每种类型 tr、tq 都以循环方式依赖于另一种类型。

有什么方法可以让它发挥作用吗，通过某种类型的巫术之类的？

我在 Win7 上使用 Haskell 平台 2014.2.0.0 和 GHCi 7.8.3。

Answer 1

我使用 Fix 键入 zipp 的问题（正如我在 Carsten 对的回答的评论中指出的那样）是没有任何一种语言包含 Fix类型：

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

fixList :: ([a] -> [a]) -> [a]
fixList f = (\g -> f (unFix g g)) $ Fix (\g -> f (unFix g g))

diverges :: [a]
diverges = fixList id

这似乎是一个晦涩的问题，但是用一种完整的语言来实现真的很好，因为这也构成了正式的终止证明。所以让我们在 Agda 中为 zipp 找一个类型。

首先，让我们坚持一段时间Haskell。如果我们手动展开一些固定列表的 zip1 和 zip2 的定义，我们发现所有的展开都有适当的类型，我们可以将 zip1 的任何展开应用于任何展开zip2，并且类型对齐（我们得到了正确的结果）。

-- unfold zip1 for [1, 0]
f0 k = []        -- zip1 []
f1 k = k 0 f0    -- zip1 [0]
f2 k = k 1 f1    -- zip1 [1, 0]

-- unfold zip2 for [5, 3]
g0 x r = []               -- zip2 []
g1 x r = (x, 3) : r g0    -- zip2 [3]
g2 x r = (x, 5) : r g1    -- zip2 [3, 5]

-- testing
f2 g2 -- [(1, 5), (0, 3)]
f2 g0 -- []

-- looking at some of the types in GHCI
f0 :: t -> [t1]
f1 :: Num a => (a -> (t1 -> [t2]) -> t) -> t
g0 :: t -> t1 -> [t2]
g1 :: Num t1 => t -> ((t2 -> t3 -> [t4]) -> [(t, t1)]) -> [(t, t1)]

我们推测对于zip1-s 和zip2-s 的任何特定组合，类型可以统一，但我们无法表达这与通常的 foldr 一样，因为所有展开都有无数种不同的类型。所以我们现在切换到 Agda。

一些预备知识和依赖项的通常定义 foldr:

open import Data.Nat
open import Data.List hiding (foldr)
open import Function
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Data.Product

foldr :
    {A : Set}
    (B : List A → Set)
  → (∀ {xs} x → B xs → B (x ∷ xs))
  → B []    
  → (xs : List A)
  → B xs
foldr B f z []       = z
foldr B f z (x ∷ xs) = f x (foldr B f z xs)

我们注意到展开的类型取决于待压缩列表的长度，因此我们编写了两个函数来生成这些类型。 A 是第一个列表元素的类型，B 是第二个列表元素的类型，C 是我们到达时忽略的参数的参数列表的末尾。 n当然是列表的长度。

Zip1 : Set → Set → Set → ℕ → Set
Zip1 A B C zero    = C → List (A × B)
Zip1 A B C (suc n) = (A → Zip1 A B C n → List (A × B)) → List (A × B)

Zip2 : Set → Set → Set → ℕ → Set
Zip2 A B C zero    = A → C → List (A × B)
Zip2 A B C (suc n) = A → (Zip2 A B C n → List (A × B)) → List (A × B)

我们现在需要证明我们确实可以将任何 Zip1 应用于任何 Zip2，并得到一个 List (A × B) 作为结果。

unifyZip : ∀ A B n m → ∃₂ λ C₁ C₂ → Zip1 A B C₁ n ≡ (Zip2 A B C₂ m → List (A × B))
unifyZip A B zero    m       = Zip2 A B ⊥ m , ⊥ , refl
unifyZip A B (suc n) zero    = ⊥ , Zip1 A B ⊥ n , refl
unifyZip A B (suc n) (suc m) with unifyZip A B n m
... | C₁ , C₂ , p = C₁ , C₂ , cong (λ t → (A → t → List (A × B)) → List (A × B)) p

英文unifyZip的类型："for all A and B types and n and m natural numbers, there exist some C₁ and C₂ types such that Zip1 A B C₁ n is a function from Zip2 A B C₂ m to List (A × B)".

证明本身很简单；如果我们到达任一拉链的末端，我们将空拉链的输入类型实例化为另一个拉链的类型。使用空类型 (⊥) 表明该参数的类型选择是任意的。在递归的情况下，我们只是将等式证明增加一步迭代。

现在我们可以写zipp:

zip1 : ∀ A B C (as : List A) → Zip1 A B C (length as)
zip1 A B C = foldr (Zip1 A B C ∘ length) (λ x r k → k x r) (λ _ → [])

zip2 : ∀ A B C (bs : List B) → Zip2 A B C (length bs)
zip2 A B C = foldr (Zip2 A B C ∘ length) (λ y k x r → (x , y) ∷ r k) (λ _ _ → [])

zipp : ∀ {A B : Set} → List A → List B → List (A × B)
zipp {A}{B} xs ys with unifyZip A B (length xs) (length ys)
... | C₁ , C₂ , p with zip1 A B C₁ xs | zip2 A B C₂ ys
... | zxs | zys rewrite p = zxs zys

如果我们眯着眼睛尝试忽略代码中的证明，我们会发现 zipp 在操作上确实与 Haskell 定义相同。事实上，在所有可擦除证明被擦除后，代码变得完全一样。 Agda 可能不会执行此擦除操作，但 Idris 编译器肯定会执行。

（作为旁注，我想知道我们是否可以在融合优化中使用像 zipp 这样的聪明函数。zipp 似乎比 Oleg Kiselyov 的 fold zipping. 更有效但是zipp 似乎没有 System F 类型；也许我们可以尝试将数据编码为依赖消除器（归纳原理）而不是通常的消除器，并尝试融合这些表示？）

Answer 2

应用来自 , I was able to solve it 的见解，通过定义两个相互递归的类型：

-- tr ~ tq -> [(a,b)]
-- tq ~ a -> tr -> [(a,b)]

newtype Tr a b = R { runR ::  Tq a b -> [(a,b)] }
newtype Tq a b = Q { runQ ::  a -> Tr a b -> [(a,b)] }

zipp :: [a] -> [b] -> [(a,b)]
zipp xs ys = runR (zip1 xs) (zip2 ys)
  where
     zip1 = foldr (\ x r -> R $ \q -> runQ q x r ) n 
     n = R (\_ -> [])

     zip2 = foldr (\ y q -> Q $ \x r -> (x,y) : runR r q ) m 
     m = Q (\_ _ -> [])

main = print $ zipp [1..3] [10,20..]
-- [(1,10),(2,20),(3,30)]

从类型等价到类型定义的转换纯粹是机械的，所以也许编译器也可以为我们做这件事！

仅使用 foldr 定义 zip 时出现无限类型错误；可以修复吗？

Infinite type error when defining zip with foldr only; can it be fixed?

haskell

types

fold