Thanks Claus, Indeed the problem was that I was using the Strict state monad, with lazy state it does the right thing when run through testP. I will try and get back to this thread if I manage the derivation which "proves" (or at least supports) that the two versions are equivalent.
2009/4/4 Claus Reinke <claus.rei...@talk21.com>: >> takeListSt' = evalState . foldr k (return []) . map (State . splitAt) >> where k m m' = cutNull $ do x<-m; xs<-m'; return (x:xs) >> cutNull m = do s<-get; if null s then return [] else m > > |Not only is ths not that elegant anymore, > As I was saying, sequence/mapM with early cutout is common > enough that one might want it in the libraries, which would return > this variant into readability again. > > |I think it *still* has a bug, stack overflow against > > That would really surprise me. Not that it is impossible - as I was > also saying, I haven't replayed the derivation for the modified code. > However, the modification was arrived at by taking the original > derivation, seeing where its result deviated from the explicitly > recursive specification, and spotting the aspect of the implicitly > recursive version that was responsible for the deviation. > Of course, the derivation itself could have an error, but equating the > functions themselves gives me rather more confidence/coverage than any > finite number of tests could. If I were to enter the derivation > into a proof checking tool and be successful, that would further raise > the level of confidence/coverage (leaving bugs in the proof checker). > > Note that I'm not asking whether the original spec did the "right" > thing, only whether or not the variations "correctly" do the same > thing as the original spec. > > |testP pf = mapM_ putStrLn [ > | show $ take 5 $ pf (repeat 0) [1,2,3] > | , show $ pf ( take 1000 [3,7..] ) [1..100] > | , show . pf [3,7,11,15] $ ( take (10^6) [1..]) > | , show . head . last $ pf (take 1000 $ [3,3..]) [1..10^6] > | ] > | > |where the first test (with take 5) is new. > |whereas the version with explicit recursion and pattern matching > |doesn't suffer from this problem > > I get identical results for 'takeListSt'' and the original 'takeList1' > (code repeated below). > It took me a couple of moments to remember that you had been playing with > Control.Monad.State.Strict instead of the default > Control.Monad.State(.Lazy). That would invalidate the original derivation > (different definition of '>>=', therefore a different end result after > unfolding '>>='), let alone the modified code based on it. > If you replay the derivation, taking the strictness variations into account, > you should arrive at an explicitly recursive version that > differs from the spec. Which might make it easier to see what > the difference is. > > |partitions [] xs = [] > |partitions (n:parts) xs = > | let (beg,end) = splitAt n xs > | in beg : ( case end of > | [] -> [] > | xs -> partitions parts xs) > > That version cannot be transformed into the original spec, because > it doesn't define the same function. As I mentioned: > >> (btw, both 'takeListSt'' and 'takeListSc'' pass Thomas' 'testP', as does >> his 'partitions', but 'partitions' is not the same function as 'takeList': >> consider 'null $ takeList [1] undefined' and 'takeList [0] []' ;-) > > With the original spec > > takeList1 [] _ = [] > takeList1 _ [] = [] > takeList1 (n : ns) xs = h : takeList1 ns t > where (h, t) = splitAt n xs > > and 'takeList4' being your 'partitions', we get: > > *Main> null $ takeList1 [1] undefined > *** Exception: Prelude.undefined > *Main> null $ takeList4 [1] undefined > False > *Main> takeList1 [0] [] > [] > *Main> takeList4 [0] [] > [[]] > >> I am starting to think that the tricky part in all these functions is >> that by using higher order functions from the prelude, you sweep the >> failure case under the rug. > > Yes, the reason that more abstract functions are useful is that they > hide irrelevant details, allowing us to spend our limited capacity on > relevant details. If all abstract functions happen to hide details that > matter, more concrete functions that expose those details can be more > helpful. > But even that has to be qualified: for instance, at first I found it easier > to see the issues with the original 'State' variant in its transformed, > explicitly recursive version, but after the derivation had convinced me that > there was no magic going on, I realized that it was just the old 'mapM' > doesn't stop early issue. So I could have seen the issue in the abstract > form, but my mind (and apparently other minds, too;-) refused to think about > the cornercases there until prompted. > If not for this tendency to ignore details that might be relevant, the > abstract code would provide an abstract treatment of the failure case as > well: instead of working out the details by trying to find useful tests for > the explicit pattern matches, we can just look at > wether the definition uses 'mapM' or 'mapMWithCut', or whether > it uses 'Control.Monad.State' or 'Control.Monad.State.Strict'. > > Just exposing all the details all the time isn't going to help, as the > 'partition' example demonstrates: we might still ignore the relevant > details, this time not because they are hidden in abstractions, but > because they are hidden in other irrelevant details. There really > isn't a single view of software that will serve all purposes, one > has to find appropriate views for every task, including using > multiple views of the same piece of software. Which is where > program transformation comes in handy!-) > >> Specifically, what happens when splitAt n doesn't have a list of length n? >> The answer isn't in fact obvious at all. I can think of three things that >> could hapen. > > I agree that the "right" thing to do can be a matter of dispute, and > so I based my definition of "correct" on equivalence to a specific version > of the code, the first explicitly recursive version I could find > ('takeList1' above). > > Claus > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe