[Haskell-cafe] lengthOP rewrite rules

[Lennart Augustsson]

There is nothing "better" about terminating more often.  Either your
transformation has the same semantics as the original, in which case
it is correct.  Or your transformation has different sematics than the
original, in which case it's incorrect.

  -- Lennart

On Fri, Dec 19, 2008 at 3:03 AM, wren ng thornton <wren at freegeek.org> wrote:
> 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
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>