
Am 14.01.2009 um 15:26 schrieb Henning Thielemann:
See the List functions in http://hackage.haskell.org/cgi-bin/hackage-scripts/package/ utility-ht
Version 0.0.1 was before applying StrictCheck, 0.0.2 after processing its suggestions. I have stopped when I saw that it repeatedly shows examples where I expect, that they are unresolvable.
Thanks very much. Your library has provided me with an invaluable insight. The original example from the IFL paper that showed problems with lists is reverse. StrictCheck states the following You have to fulfil f _|_ = _|_ f (_|_ : _|_) = _|_ -> (_|_ : _|_) f (_|_ : []) = (_|_ : []) f (_|_ : (_|_ : _|_)) = _|_ -> (_|_ : (_|_ : _|_)) f (_|_ : (_|_ : [])) = (_|_ : (_|_ : [])) f (_|_ : (_|_ : (_|_ : _|_))) = _|_ -> (_|_ : (_|_ : (_|_ : _|_))) That is, if the argument of reverse is known to have at least 2 elements the result should have at least two elements. The only implementation I could imagine that fulfilled these requirements had a quadratic complexity. But your shorterList inspired me to an implementation that is not as efficient as the original one but which is linear. That is, there is a least strict implementation of reverse that is nearly as efficient as the standard implementation. withSpineOf :: [a] -> [a] -> [a] _ `withSpineOf` [] = [] l `withSpineOf` (_:ys) = x:xs `withSpineOf` ys where x:xs = l rev xs = reverse xs `withSpineOf` xs If anybody knows a prettier implementation of reverse that is least- strict I would be delighted to hear about it. By the way, I was wrong that your example is similar to the reverse example. My new implementation of StrictCheck states that maybePrefixOf is least strict. Cheers, Jan