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'.
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
