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

Question

(对于上下文,请参阅最近的SO条目).

我试图想出的定义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对前一个问题的回答的评论中所指出的)是没有总语言包含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

这可能看起来是一个模糊的问题,但实际上使用全语言实现真的很好,因为这也构成了终止的正式证明.所以让我们zipp在Agda中找到一个类型.

首先,让我们坚持一下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)]

我们猜想类型可以统一为-s和-s的任何特定组合,但我们不能用通常的方式来表达,因为所有展开都有无数种不同的类型.所以我们现在切换到Agda.zip1zip2foldr

一些预备和依赖的通常定义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的折叠拉链更有效.但zipp似乎没有System F类型;也许我们可以尝试编码数据作为依赖消除器(归纳原理)而不是通常的消除器,并尝试融合这些表示？)

Answer 2

应用我的其他答案中的见解，我能够通过定义两种相互递归类型来解决它：

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

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