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
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