Luke Palmer wrote:
This does not answer your question, but you can solve this problem without
rewrite rules by having length return a lazy natural:
data Nat = Zero | Succ Nat
And defining lazy comparison operators on it.
And if you want to go that route, then see Data.List.Extras.LazyLength
from list-extras[1]. Peano integers are quite inefficient, but this
library does the same transform efficiently.
[1] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/list-extras
Of course you cannot replace usages of Prelude.length. But I am really not
in favor of rules which change semantics, even if they only make things less
strict. My argument is the following. I may come to rely on such
nonstrictness as in:
bad xs = (length xs > 10, length xs > 20)
bad [1..] will return (True,True). However, if I do an obviously
semantics-preserving refactor:
bad xs = (l > 10, l > 20)
where
l = length xs
My semantics are not preserved: bad [1..] = (_|_, _|_) (if/unless the
compiler is clever, in which case my semantics depend on the compiler's
cleverness which is even worse)
Data.List.Extras.LazyLength does have rewrite rules to apply the lazy
versions in place of Prelude.length where it can. My justification is
two-fold. First is that for finite lists the semantics are identical but
the memory behavior is strictly better. Second is that for non-finite
lists the termination behavior is strictly better.
It's true that refactoring can disable either point, and that can alter
semantics in the latter case. Since the module is explicit about having
these rules, I would say that users should remain aware of the fact that
they're taking advantage of them or they should use the explicit
lengthBound or lengthCompare functions instead.
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
