RE: [Haskell] How to zip folds: A library of fold transformers
Oleg: I'm sure you're aware of the close connection between your FR stuff (nice) and the foldr/build list-fusion work? (So-called "short-cut deforestation".) To make short-cut deforestation work, one has to write map, filter etc in precisely the style you give. I have not grokked your zip idea, though it looks cunning. I wonder if it could be formulated in such a way that we could do foldr/build fusion down both branches of a zip? John Launchbury et al had a paper about hyper-functions which tackled the zip problem too. http://citeseer.ist.psu.edu/krstic01hyperfunctions.html. Also Josef Svengingsson (ICFP'02). I don't know how these relate to your solution. Simon | -----Original Message----- | From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of | oleg@pobox.com | Sent: 12 October 2005 01:25 | To: haskell@haskell.org | Subject: [Haskell] How to zip folds: A library of fold transformers | | | We show how to merge two folds into another fold | `elementwise'. Furthermore, we present a library of (potentially | infinite) ``lists'' represented as folds (aka streams, aka | success-failure-continuation--based generators). Whereas the standard | Prelude functions such as |map| and |take| transform lists, we | transform folds. We implement the range of progressively more complex | transformers -- from |map|, |filter|, |takeWhile| to |take|, to |drop| | and |dropWhile|, and finally, |zip| and |zipWith|. | | Emphatically we never convert a stream to a list and so we never use | value recursion. All iterative processing is driven by the fold | itself. | | The implementation of zip also solves the problem of ``parallel | loops''. One can think of a fold as an accumulating loop. One can | easily represent a nested loop as a nested fold. Representing parallel | loop as a fold is a challenge, answered at the end of the message. We | need recursive types -- but again, never value recursion. | | This library is inspired by Greg Buchholz' message on the Haskell-Cafe list | and is meant to answer open questions posed at the end of that message | http://www.haskell.org/pipermail/haskell-cafe/2005-October/011575.html | | This message a complete literate Haskell code. | | > {-# OPTIONS -fglasgow-exts #-} | > module Folds where | | First we define the representation of a list as a fold: | | > newtype FR a = FR (forall ans. (a -> ans -> ans) -> ans -> ans) | > unFR (FR x) = x | | It has a rank-2 type. The defining equations are: if flst is a value | of a type |FR a|, then | unFR flst f z = z if flst represents an empty list | unFR flst f z = f e (unFR flst' f z) | if flst represents the list with the head 'e' | and flst' represents the rest of that list | | >From another point of view, |unFR flst| can be considered a _stream_ | that takes two arguments: the success continuation of the type | |a -> ans -> ans| and the failure continuation of the type |ans|. The LogicT | paper discusses such types in detail, and shows how to find that "rest | of the list" flst'. The slides of the ICFP05 presentation by | Chung-chieh Shan point out to more related work in that area. | | But we are here to drop, take, dropWhile, etc. Our functions will | take a stream and return another stream, of the |FR a| type, which | represents truncated, filtered, etc. source stream. | | Let us define two sample streams: a finite and an infinite one: | | > stream1 :: FR Char | > stream1 = FR (\f unit -> foldr f unit ['a'..'i']) | > stream2 :: FR Int | > stream2 = FR (\f unit -> foldr f unit [1..]) | | and the way to show the stream. This is the only time we convert |FR a| | to a list -- so we can more easily show it. | | > instance Show a => Show (FR a) where | > show l = show $ unFR l (:) [] | | | The map function is trivial: | | > smap :: (a->b) -> FR a -> FR b | | *> smap f l = FR(\g -> unFR l (g . f)) | | which can also be written as | | > smap f l = FR((unFR l) . (flip (.) f)) | | For example, | | > test1 = show $ smap succ stream1 | | | Next is the filter function: | | > sfilter :: (a -> Bool) -> FR a -> FR a | > sfilter p l = FR(\f -> unFR l (\e r -> if p e then f e r else r)) | | > test2 = sfilter (not . (`elem` "ch")) stream1 | | The function takeWhile is quite straightforward, too | | > stakeWhile :: (a -> Bool) -> FR a -> FR a | > stakeWhile p l = FR(\f z -> unFR l (\e r -> if p e then f e r else z) z) | | > test3 = stakeWhile (< 'z') stream1 | > test3' = stakeWhile (< 10) stream2 | | As we can see, stakeWhile well applies to an infinite stream. | | The functions take, drop, dropWhile ask for more complexity. | | > stake :: (Ord n, Num n) => n -> FR a -> FR a | > stake n l = FR(\f z -> | > unFR l (\e r n -> if n <= 0 then z else f e (r (n-1))) (const z) n) | | > test4 = stake 20 stream1 | > test4' = stake 5 stream1 | > test4'' = stake 11 stream2 | > test4''' = (stake 11 . smap (^2)) stream2 | | The function sdrop shows the major deficiency: we're stuck with the | (<=0) test for the rest of the stream. In this case, some delimited | continuation operators like `control' can help, in limited | circumstances. | | > 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) | | > test5 = sdrop 20 stream1 | > test5' = sdrop 5 stream1 | > test5'' = stake 5 $ sdrop 11 stream2 | | The function dropWhile becomes straightforward | | > sdropWhile :: (a -> Bool) -> FR a -> FR a | > sdropWhile p l = FR(\f z -> | > unFR l (\e r done -> | > if done then f e (r done) | > else if p e then r done else f e (r True)) (const z) False) | | > test6 = sdropWhile (< 'z') stream1 | > test6' = sdropWhile (< 'd') stream1 | > test6'' = stake 5 $ sdropWhile (< 10) stream2 | | The zip function is the most complex. | | Here we need a recursive type: an iso-recursive type to emulate the | equi-recursive one. | | > newtype RecFR a ans = RecFR (a -> (RecFR a ans -> ans) -> ans) | > unRecFR (RecFR x) = x | | This is still a newtype: there is no extra consing. | | I will not pretend that the following is the most perspicuous piece of code: | | *> szip :: FR a1 -> FR a2 -> FR (a1,a2) | *> szip l1 l2 = FR(\f z -> | *> let l1' = unFR l1 (\e r x -> unRecFR x e r) (\r -> z) | *> l2' = unFR l2 (\e2 r2 e1 r1 -> f (e1,e2) (r1 (RecFR r2))) (\e r-> z) | *> in l1' (RecFR l2')) | | It can be simplified to the following: | | > szipWith :: (a->b->c) -> FR a -> FR b -> FR c | > szipWith t l1 l2 = FR(\f z -> | > unFR l1 (\e r x -> unRecFR x e r) (\x -> z) | > (RecFR $ | > unFR l2 (\e2 r2 e1 r1 -> f (t e1 e2) (r1 (RecFR r2))) (\e r -> z))) | > | > szip :: FR a -> FR b -> FR (a,b) | > szip = szipWith (,) | | | One can easily prove that this function does correspond to zip for all | finite streams. The proof for infinite streams requires more | elaboration. | | > test81 = szip stream1 stream1 | > test82 = szip stream1 stream2 | > test83 = szip stream2 stream1 | > test84 = stake 5 $ szip stream2 (sdrop 10 stream2) | | As one may expect (or not), these tests give the right results | | *Folds> test83 | [(1,'a'),(2,'b'),(3,'c'),(4,'d'),(5,'e'),(6,'f'),(7,'g'),(8,'h'),(9,'i') ] | *Folds> test84 | [(1,11),(2,12),(3,13),(4,14),(5,15)] | | _______________________________________________ | Haskell mailing list | Haskell@haskell.org | http://www.haskell.org/mailman/listinfo/haskell
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'.
participants (2)
-
oleg＠pobox.com -
Simon Peyton-Jones