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

Question

（有关上下文，请参阅this recent SO entry）。

我试图仅使用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
-}

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

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 的回答的cmets 中指出的那样）是没有总语言包含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) 的函数。

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

现在我们可以写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

应用来自my other answer 的见解，我能够通过定义两个相互递归的类型来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)]

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