<p dir="ltr">Your approach points the way very clearly toward the proper inductive argument as well, so I will look into that when I get home from the dentist. Assuming all goes as planned, you seem to have a winner. One thing that caught my eye in your benchmark report: it looked to me like initsQ2 was very slightly slower than initsQ on the NF tests. Do you think you could do some bigger tests there and see if it's real? If so, my *guess* is that the scanl' is wasting time forcing things that have already been forced, which we probably can't do anything about but should bear in mind.</p>
<p dir="ltr">David Feuer</p>
<div class="gmail_quote">On Jul 24, 2014 10:02 AM, "Joachim Breitner" <<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi David,<br>
<br>
Am Mittwoch, den 23.07.2014, 16:17 -0400 schrieb David Feuer:<br>
> In a comment on trac #9345, nomeata proposed the implementation of<br>
> Data.List.inits below. He indicates that the performance is very good,<br>
> and wrote it in this fashion so it could fuse. My concern is that<br>
> since seq is used in the argument to build, we need to make sure that<br>
> fusion on the left will be safe. If I did the calculations right, this<br>
> specifically requires that for all f, cons, nil, and bs, and all a≠_|<br>
> _, the following "correct" expression<br>
<br>
> e1 = a `cons`<br>
> foldr cons nil $<br>
> foldr (\b g x -> (let b' = f x b in b' `seq` (b' : g b')))<br>
> (\b -> b `seq` [])<br>
> bs<br>
> a<br>
><br>
> gives the same result as the fused expression<br>
><br>
> e2 = a `cons`<br>
> foldr (\b g x -> (let b' = f x b in b' `seq` (b' `cons` g b')))<br>
> (\b -> b `seq` nil)<br>
> bs<br>
> a<br>
><br>
> I haven't been able to figure out how to prove this or give a<br>
> counterexample, so far, but I have very little experience with such.<br>
><br>
> myScanl' :: (b -> a -> b) -> b -> [a] -> [b]<br>
> myScanl' f a bs = build $ \c n -><br>
> a `seq` a `c`<br>
> foldr (\b g x -> (let b' = f x b in b' `seq` (b' `c` g b')))<br>
> (\b -> b `seq` n)<br>
> bs<br>
> a<br>
<br>
I don’t have much experience either, but let’s try.<br>
<br>
First of all, let’s simplify it a bit. It is unlikely that the problem<br>
will appear for lists of varying length. Since all finite lists are<br>
one-element-lists¹, let us substitute bs = [b]:<br>
<br>
myScanl' f a [b]<br>
==<br>
build $ \c n -><br>
a `seq` a `c`<br>
foldr (\b g x -> (let b' = f x b in b' `seq` (b' `c` g b')))<br>
(\b -> b `seq` n)<br>
(b : [])<br>
a<br>
== simplifying foldr<br>
build $ \c n -><br>
a `seq` a `c`<br>
(\ x -> let b' = f x b<br>
in b' `seq` (b' `c` (b' `seq` n)))<br>
a<br>
== more β-reduction, redundant seq<br>
build $ \c n -><br>
a `seq` a `c`<br>
let b' = f a b<br>
in b' `seq` (b' `c` n)<br>
<br>
<br>
Now let’s calculate the expression<br>
foldr c n $ myScanl' f a [b]<br>
without and with fusion.<br>
<br>
before_fusion<br>
==<br>
foldr c n $ myScanl' f a [b]<br>
==<br>
foldr c n $ a `seq` (a : let b' = f a b in b' `seq` (b' : []))<br>
== foldr is strict in its third argument, so it commutes with seq<br>
a `seq` foldr c n $ (a : let b' = f a b in b' `seq` (b' : []))<br>
== foldr on cons<br>
a `seq` a `c` (foldr c n $ let b' = f a b in b' `seq` (b' : []))<br>
== foldr commutes with let and seq<br>
a `seq` a `c` (let b' = f a b in b' `seq` (foldr c n $ b' : []))<br>
== foldr on cons and []<br>
a `seq` a `c` (let b' = f a b in b' `seq` (b' `c` n))<br>
<br>
<br>
after_fusion<br>
==<br>
(\c n -> a `seq` a `c` let b' = f a b in b' `seq` (b' `c` n)) c n<br>
==<br>
a `seq` a `c` (let b' = f a b in b' `seq` (b' `c` n))<br>
<br>
So they yield the same results, independent of c and n. This includes<br>
the counter example from “Free Theorems in the Presence of seq”, (c =<br>
seq, n = []).<br>
<br>
Judging from this I conclude that nothing can go wrong for finite lists.<br>
What about partial lists, i.e. bs = b : ⊥?<br>
<br>
myScanl' f a (b : ⊥)<br>
==<br>
build $ \c n -><br>
a `seq` a `c`<br>
foldr (\b g x -> (let b' = f x b in b' `seq` (b' `c` g b')))<br>
(\b -> b `seq` n)<br>
(b : ⊥)<br>
a<br>
== simplifying foldr<br>
build $ \c n -><br>
a `seq` a `c`<br>
(\ x -> let b' = f x b<br>
in b' `seq` (b' `c` (b' `seq` ⊥)))<br>
a<br>
== more β-reduction, redundant seq<br>
build $ \c n -><br>
a `seq` a `c`<br>
let b' = f a b<br>
in b' `seq` (b' `c` ⊥)<br>
<br>
<br>
before_fusion<br>
==<br>
foldr c n $ myScanl' f a (b:⊥)<br>
==<br>
foldr c n $ a `seq` (a : let b' = f a b in b' `seq` (b' : ⊥))<br>
== foldr is strict in its third argument, so it commutes with seq<br>
a `seq` foldr c n $ (a : let b' = f a b in b' `seq` (b' : ⊥))<br>
== foldr on cons<br>
a `seq` a `c` (foldr c n $ let b' = f a b in b' `seq` (b' : ⊥))<br>
== foldr commutes with let and seq<br>
a `seq` a `c` (let b' = f a b in b' `seq` (foldr c n $ b' : ⊥))<br>
== foldr on cons and []<br>
a `seq` a `c` (let b' = f a b in b' `seq` (b' `c` ⊥))<br>
<br>
<br>
after_fusion<br>
==<br>
(\c n -> a `seq` a `c` let b' = f a b in b' `seq` (b' `c` ⊥)) c n<br>
==<br>
a `seq` a `c` (let b' = f a b in b' `seq` (b' `c` ⊥))<br>
<br>
<br>
So nothing fancy happening here either. I conclude that we are safe, and<br>
my gut feeling tell me the reason is likely that we don’t `seq` anything<br>
built from the unknown c and n.<br>
<br>
Greetings,<br>
Joachim<br>
<br>
<br>
¹ citation needed<br>
<br>
--<br>
Joachim “nomeata” Breitner<br>
<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a> • <a href="http://www.joachim-breitner.de/" target="_blank">http://www.joachim-breitner.de/</a><br>
Jabber: <a href="mailto:nomeata@joachim-breitner.de">nomeata@joachim-breitner.de</a> • GPG-Key: 0xF0FBF51F<br>
Debian Developer: <a href="mailto:nomeata@debian.org">nomeata@debian.org</a><br>
<br>
<br>_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/libraries" target="_blank">http://www.haskell.org/mailman/listinfo/libraries</a><br>
<br></blockquote></div>