Thomas Hartman wrote:
Luke, does your explanation to Guenther have anything to do with coinduction? -- the property that a producer gives a little bit of output at each step of recursion, which a consumer can than crunch in a lazy way?
It has more to do with "tying the knot" (using laziness to define values in terms of themselves), though there are similarities. Take the function: infZipWith f ~(x:xs) ~(y:ys) = f x y : infZipWith f xs ys which we could write less clearly as: infZipWith f xxs yys = f (head xxs) (head yys) : infZipWith f (tail xxs) (tail yys) The trick is that we can emit the thunk for f(head xxs)(head yys) without knowing what values xxs and yys actually contain--- they could still be _|_! The hope is that by the time we get to where someone asks for the value of that thunk ---by that point--- we *will* know enough about xxs and yys that we can give an answer. For knot tying to work, we must ensure that we don't ask for things "from the future" before we've actually created them. If we do, then the function will diverge, i.e. _|_. This shares similarities with the ideal 1-to-1 producer/consumer role for deforestation (whence, similarities to coinduction). -- Live well, ~wren