Why Haskell doesn't accept my combinatoric "zip" definition?

Question

This is the textbook zip function:

zip :: [a] -> [a] -> [(a,a)]
zip [] _ = []
zip _ [] = []
zip (x:xs) (y:ys) = (x,y) : zip xs ys

I asked on #haskell earlier wether "zip" could be implemented using "foldr" alone, no recursion, no pattern matching. After some thinking, we noticed the recursion could be eliminated using continuations:

zip' :: [a] -> [a] -> [(a,a)]
zip' = foldr cons nil
    where
        cons h t (y:ys) = (h,y) : (t ys)
        cons h t []     = []
        nil             = const []

We are still left with pattern matching. After some more neuron toasting I came up with an incomplete answer that I thought was logical:

zip :: [a] -> [a] -> [a]
zip a b = (zipper a) (zipper b) where
    zipper = foldr (\ x xs cont -> x : cont xs) (const [])

It returns a flat list, but does the zipping. I was certain it made sense, but Haskell complained about the type. I proceeded to test it on a untyped lambda calculator, and it worked. Why can't Haskell accept my function?

The error is:

zip.hs:17:19:
    Occurs check: cannot construct the infinite type:
      t0 ~ (t0 -> [a]) -> [a]
    Expected type: a -> ((t0 -> [a]) -> [a]) -> (t0 -> [a]) -> [a]
      Actual type: a
                   -> ((t0 -> [a]) -> [a]) -> (((t0 -> [a]) -> [a]) -> [a]) -> [a]
    Relevant bindings include
      b ∷ [a] (bound at zip.hs:17:7)
      a ∷ [a] (bound at zip.hs:17:5)
      zip ∷ [a] -> [a] -> [a] (bound at zip.hs:17:1)
    In the first argument of ‘foldr’, namely ‘cons’
    In the expression: ((foldr cons nil a) (foldr cons nil b))

zip.hs:17:38:
    Occurs check: cannot construct the infinite type:
      t0 ~ (t0 -> [a]) -> [a]
    Expected type: a -> (t0 -> [a]) -> t0 -> [a]
      Actual type: a -> (t0 -> [a]) -> ((t0 -> [a]) -> [a]) -> [a]
    Relevant bindings include
      b ∷ [a] (bound at zip.hs:17:7)
      a ∷ [a] (bound at zip.hs:17:5)
      zip ∷ [a] -> [a] -> [a] (bound at zip.hs:17:1)
    In the first argument of ‘foldr’, namely ‘cons’
    In the fourth argument of ‘foldr’, namely ‘(foldr cons nil b)’

Answer 1

As to why your definition is not accepted: look at this:

λ> :t \ x xs cont -> x : cont xs
 ... :: a -> r -> ((r -> [a]) -> [a])

λ> :t foldr
foldr :: (a' -> b' -> b') -> b' -> [a'] -> b'

so if you want to use the first function as an argument for foldr you get (if you match the types of foldrs first argument:

a' := a
b' := r
b' := (r -> [a]) -> [a]

which of course is a problem (as r and (r -> [a]) -> [a] mutual-recursive and should both be equal to b' )

That is what the compiler tells you

how to repair it

You can repair your idea using

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

which I borrowed form it original use.

With this you can write:

zipCat :: [a] -> [a] -> [a]
zipCat a b = (unFix $ zipper a) (zipper b) where
  zipper = foldr foldF (Fix $ const [])
  foldF x xs = Fix (\ cont -> x : (unFix cont $ xs))

and you get:

λ> zipCat [1..4] [5..8]
[1,5,2,6,3,7,4,8]

which is (what I think) you wanted.

BUT obvious here both of your lists needs to be of the same type so I don't know if this will really help you

Answer 2

We can eliminate the explicit pattern matching by defining a function that will do it for us.

Is it cheating? Not if maybe and bool are allowed, as they are; then we should also allow list (also in extra's Data.List.Extra),

list :: b -> (a -> [a] -> b) -> [a] -> b 
list n c []     = n
list n c (x:xs) = c x xs

just the same; so that we can have, in your zip' definition,

cons h t = list [] (\y ys -> (h,y) : t ys)

or e.g.

         = list [] (uncurry ((:).(h,).fst <*> t.snd))
         = list [] (curry $ uncurry (:) . ((h,) *** t))
         = list [] (flip ((.) . (:) . (h,)) t)
         = list [] ((. t) . (:) . (h,))

if you prefer this kind of thing.

About your error, "infinite type" often indicates self application; indeed, whatever your zipper returns, you're self-applying it, in your

zip a b = (zipper a) (zipper b)  where ....

---

I tried to tweak your definition and came up with

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 seems to reduce correctly on paper, but still I got the infinite type errors here too.

There is no (immediately apparent) self-application now, but the type of the continuation that the first zip gets, depends on the type of that first zip itself; so still there's a circular dependency: tq is on both sides of the type equivalency in tq ~ a -> tr -> [(a,b)] ~ a -> (tq -> [(a,b)]) -> [(a,b)].

Indeed that's the two type errors that I get, (the first one is about the tr 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

In the usual definitions using foldr with continuations, the type of those continuations is independent; that's the reason that it works there, I guess.

• See also my second answer here, and this follow-up Q&A

Answer 3

I can offer you a slightly different perspective (I think) to arrive at a similar solution as Carsten's (but with simpler types).

Here's your code again, for your "weaving zip" (I'm writing tr for "the type of r", similarly tq for "the type of q"; I always use "r" for the recursive result argument of combining function in foldr definitions, as a mnemonic device):

zipw :: [a] -> [a] -> [a]
zipw xs ys = (zipper xs) (zipper ys) where
    zipper xs q = foldr (\ x r q -> x : q r) (const []) xs q
                        --- c -------------- --- n ----

 -- zipper [x1,x2,x3] (zipper ys) =
 -- c x1 (c x2 (c x3 n)) (zipper ys)
         --- r --------  --- q -----  tr ~ tq ; q r :: [a]
                                      --     => r r :: [a]
                                      -- => r :: tr -> [a] 
                                      --   tr ~  tr -> [a]    

So, this is the infinite type. Haskell doesn't allow this for an arbitrary type (which is what type variables stand for).

But Haskell's datatypes do actually admit recursion. Lists, trees, etc. — all the usual types are recursive. This is allowed:

data Tree a = Branch (Tree a) (Tree a)

Here we do have the same type on both sides of the equation, just as we have tr on both sides of the type equivalency, tr ~ tr -> [a]. But it's a specific type, not an arbitrary one.

So we just declare it so, following the above "equation":

newtype TR a = Pack { unpack :: TR a -> [a] } 
           -- unpack :: TR a -> TR a -> [a]

What's a Tree a type? It's "something" that goes into a Branch, which is a Tree a. A given tree doesn't have to be infinitely constructed, because undefined has type Tree a too.

What's a TR a type? It's "something" that goes into TR a -> [a], which is a TR a. A given TR a doesn't have to be infinitely constructed, because const [] can be of type TR a too.

Our wannabe recursive type tr ~ tr -> [a] has become bona fide recursive type definition newtype TR a = Pack { TR a -> [a] }, hiding behind the data constructor, Pack (which will be gotten rid of by the compiler, thanks to the newtype keyword being used, but that's an extraneous detail; it works with data too).

Haskell handles the recursivity for us here. Type theoreticians love to deal with this themselves, with Fix and whatnot; but a Haskell user already has this available to them, in the language. We don't have to understand how it is implemented, to be able to use it. No need to reinvent the wheel until we want to build it ourselves.

So, zipper xs had type tr; now it becomes TR a, so this is what the new zipper xs must return — the "packed" list-producing function. The foldr combining function must return what the zipper call returns (by the virtues of foldr definition). To apply the packed function we now need to unpack it first:

zipw :: [a] -> [a] -> [a]
zipw xs ys = unpack (zipper xs) (zipper ys)
    where
    zipper :: [a] -> TR a
    zipper = foldr (\ x r -> Pack $ \q -> x : unpack q r)
                   (Pack $ const [])