[Haskell-cafe] is there a way to prove the equivalence of these two
implementations of (Prelude) break function?
tphyahoo at gmail.com
Sat Jun 5 23:10:20 EDT 2010
Here's two implementations of break, a snappy one from the prelude,
and a slow stupid stateful one.
They are quickchecked to be identical.
Is there a way to prove they are identical mathematically? What are
the techniques involved? Or to transform one to the other?
tThis = take 5 . show . mybreak (>4000000) $ [1..10^7]
tPrel = take 5 . show . prelbreak (>4000000) $ [1..10^7]
prelbreak p xs = (takeWhile (not . p) xs,dropWhile (not . p) xs) --
fast, more or less as implemented in prelude iiuc
mybreak p xs = evalState (brk p) (,xs) -- stateful, slow
brk p = do
(notsat,remaining) <- get
case remaining of
 -> return (notsat,remaining)
(r:rs) -> if p r
then return (notsat,remaining)
else do put (notsat++[r],rs) -- ++ is probaby a
More information about the Haskell-Cafe