#9345: Data.List.inits is extremely slow -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.8.4 Component: | Version: 7.8.3 libraries/base | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Easy (less than 1 Unknown/Multiple | hour) Type of failure: Runtime | Blocked By: performance bug | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:8 nomeata]:
That's a neat idea. If I'm not mistaken, seq in the argument to build leads to a proof obligation to justify the safety of the fusion. Do you have a proof?
No. What exactly is the proof obligation in this case?
According to the [http://www.haskell.org/haskellwiki/Correctness_of_short_cut_fusion short cut fusion page] on the Haskell Wiki, the foldr/build equivalence in general is only guaranteed when the argument to build does not use `seq`; otherwise there are ways to break it so that the fused program is less lazy than it should be. That page gives one way around that limitation, which involves restricting the other arguments to `foldr`, but that's not an option here—a "bare" `build` is exposed to the world. So if I understand things right (which is never guaranteed at all), you're left having to write your own proof, from scratch or based on other theorems not mentioned on that page, that the foldr/build rule is safe here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9345#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler