Hello!
I'm sure you're aware of the close connection between your FR stuff (nice) and the foldr/build list-fusion work?
I am now. Indeed, the 'FR' representation of lists is what one passes to 'build'. Incidentally, the higher-rank type of FR is a _requirement_ (otherwise, things won't type) rather than just a precaution to prevent 'build' from using list constructors [] and (:) internally.
Also Josef Svengingsson (ICFP'02). I don't know how these relate to your solution.
His paper is actually quite related to our ICFP'05 paper: the function `destroy' (which he re-discovered after Gill) is somewhat related to `msplit' in the LogicT paper, and the function `reflect' of LogicT paper is related to unfoldr. There are many differences however. The function `msplit' has nothing to do with Haskell lists and never uses any lists constructors, even internally. The functions msplit and reflect operate over any backtracking computation over any base monad (which may be strict, btw). The presence of the base monad makes things trickier as we now must assure that we do not repeat effects. Therefore, the equivalent of the destroy/infoldr rule of Josef Svengingsson destroy . unfoldr === id is (in ``small-step semantics'') rr (lift m >> mzero) === lift m >> mzero rr (lift m `mplus` tma) === lift m `mplus` (rr tma) where rr tm = msplit tm >>= reflect One can read 'mzero' and 'mplus' as generalized list constructors [] and (:), and read (>>=) as a flipped application. The more complex laws assure that effects are not duplicated. It is fair to say that whereas foldr/build and destroy/infoldr fusion techniques work for Haskell lists, msplit/reflect in the LogicT paper is a fusion law for a general backtracking computation over arbitrary, perhaps even strict, base monad. That computation may look nothing like list (and in fact, the LogicT paper gives an example with delimited continuations, with `abort' playing the role of nil and `shift' the role of cons). Since the previous message on the Haskell list, a better implementation of szipWith has emerged -- in the process of answering a good question posed by Chung-chieh Shan. The new solution is actually quite simple and does not use msplit/destroy at all. If we recall that we already have stake and sdrop (so that we can `split' an FR stream into the head element (stake 1) and the rest (sdrop 1)), the code for szipWith becomes trivial. One may wonder why hadn't that occurred earlier.
szipWith :: (a->b->c) -> FR a -> FR b -> FR c szipWith t l1 l2 = FR(\f z -> unFR l1 (\e1 r r2 -> unFR r2 (\e2 _ -> f (t e1 e2) (r (sdrop 1 r2))) z) (const z) l2)
szip :: FR a -> FR b -> FR (a,b) szip = szipWith (,)
Indeed, the function sdrop already did the trick of splitting the stream. And the function sdrop is quite trivial:
sdrop :: (Ord n, Num n) => n -> FR a -> FR a sdrop n l = FR(\f z -> unFR l (\e r n -> if n <= 0 then f e (r n) else r (n-1)) (const z) n)
It means that the other, more complex expressions for szipWith, some of which include `msplit'-alike in disguise, can be mechanically derived from the above via the sequence of beta-reductions. The code for szipWith is not recursive and needs no recursive types. Let us look at szipWith closer: at first blush it looks like a nested fold (``nested loop''). But then we see that the nested expression operates on the progressively shorter list l2. That is, the 'tail' of l2 becomes the 'seed' of the outer fold represented by l1. The stream FR has the type
newtype FR a = FR (forall ans. (a -> ans -> ans) -> ans -> ans)
The szipWith code demonstrates that `unFR l1' instantiates 'ans' to the type of 'l2' -- that is, to the type FR itself. We definitely have impredicativity -- the quantified type variable in FR may be instantiated to the type that is being defined by FR. Thus the higher-rank type of FR is not a nicety and is not merely a safety property -- it is a necessity. I'm afraid constructivists would be unhappy...
John Launchbury et al had a paper about hyper-functions which tackled the zip problem too. http://citeseer.ist.psu.edu/krstic01hyperfunctions.html.
But existence of hyper-functions implies the existence of the fix-point operator. I specifically wanted to avoid Y in any guise! There are several reasons: - In the pure case, there will be nothing to prove. We can always convert an FR-list to an ordinary Haskell (i.e., co-inductive) list, and back. This is an iso-morphism, so the library of FR lists is a trivial consequence of the Haskell list library. If we banish Y however, we can no longer convert Haskell lists to FR lists, and so iso-morphism is broken. BTW, the iso-morphism between FR lists and Haskell lists no longer holds if we do all operations in some monad 'm' and that monad is strict. - It would be interesting to see, constructively, how to build the full-fledged (FR)-list library and avoid general recursion. Let the FR-list be the only driver of iterations. - Related to the above: how to build a list library without Y, without recursive types. We need only higher-ranked types. The zip function is particularly interesting because it relates to 'parallel loops'. It becomes especially interesting in the case of general backtracking computations, or backtracking computations in direct style, with delimited continuations modeling `lists'.