(for the context to this see this recent SO entry).
I tried to come up with the definition of zip using foldr only:
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
-}
It "works" on paper, but gives two "infinite type" errors:
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
Evidently, each type tr, tq, depends on the other, in a circular manner.
Is there any way to make it work, by some type sorcery or something?
I use Haskell Platform 2014.2.0.0 with GHCi 7.8.3 on Win7.
Applying the insight from my other answer, I was able to solve it, by defining two mutually-recursive types:
-- 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)]
The translation from type equivalency to type definition was purely mechanical, so maybe compiler could do this for us, too!