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

Question

(上下文见 this recent SO entry )。

我试图想出 zip 的定义使用 foldr只要:

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

它在纸上“有效”，但给出了两个“无限类型”错误:

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 Platform 2014.2.0.0 和 GHCi 7.8.3。

Answer 1

我使用 Fix 输入 zipp 的问题(正如我在对 Carsten 对 prior question 的回答的评论中指出的那样)是没有总语言包含 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的类型:“对于所有的 A和 B类型以及 n和 m自然数，存在一些 C₁和 C₂类型使得 Zip1 A B C₁ n是一个函数从 Zip2 A B C₂ m 到 List (A × B)”。

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

现在我们可以写 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 似乎没有系统F 类型；也许我们可以尝试将数据编码为依赖消除器(归纳原则)而不是通常的消除器，并尝试融合这些表示？)