9

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)’
Improve this question
8
  • What's the error Haskell gives you? Commented Apr 26, 2015 at 16:05
  • If all you're stuck with is the pattern matching just use (,) as a function, and head and tail instead of (y:ys) and maybe an if/else? Commented Apr 26, 2015 at 16:07
  • 1
    btw: a very similar question was asked some time ago: stackoverflow.com/questions/235148/implement-zip-using-foldr Commented Apr 26, 2015 at 16:23
  • 5
    Oleg did it, Oleg did it! Commented Apr 26, 2015 at 16:34
  • 1
    FYI, I added an answer to a follow-up question that could technically pass as an answer for this one too. Commented Apr 28, 2015 at 21:51

3 Answers 3

Reset to default
6

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

Improve this answer
Sign up to request clarification or add additional context in comments.

6 Comments

Use of Fix is equivalent to using general recursion or a fixpoint combinator, so I think this is at odds with OP's "no recursion" criterion.
@AndrásKovács quite possible yes (although you could argue about types vs. function or that foldr might be recursive too, ...) - do you see another way to get the compiler to accept the OP's zip that don't stray away to much from the code?
I haven't looked at OP's code yet... As to foldr, it's about as non-recursive as it can get, since it corresponds to both Church encoded lists in System F (and everything provably terminates there), and the computation rule for lists in type theory.
@AndrásKovács tbh: I think this is not the place to argue but AFAIK foldr is still implemented in a recursive fashion (in Haskell) - but again that's not really the point here is it?
@AndrásKovács (and the others...) Hi, I've added a new answer, maybe you'd like to check it out. It uses a simpler recursive type (t is actually redundant), and Haskell already has recursive types, so I don't need to think about "Fix" myself!
|
2

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 [])
Improve this answer

8 Comments

nice - yeah the t is redundant - tbh: I just used the quick copy&paste the compiler output and Fix it solution ;)
@CarstenKönig thanks; :) I thought to use this insight in the other problem; no luck for now. the types are more complex...
yeah guess so - but it should be really easy to translate [a,b,c,d,e] -> [(a,b),(c,d),...] and mix in some ADT (Either comes to mind)
@CarstenKönig I got it! I define two mutually-recursive types: ideone.com/tgAK0A. Will post the answer shortly!!
no offense meant - I have no problem if you add another answer - it just looks strange to have 4 answers where 3 are from the same person - but congrats - good job
|
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.

Improve this answer

Comments

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.