Jan Christiansen jac at informatik.uni-kiel.de
Fri Jan 16 11:45:14 EST 2009

```Am 14.01.2009 um 15:26 schrieb Henning Thielemann:

> See the List functions in
> 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
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
```