oh, btw I am using GHC 6.10.1 (on Linux x86_64) 2008/12/18 Cetin Sert

Hi,

I tested the following, why does the rewrite rules not fire when using tuples also in testRewrite2, testRewriteReverse2? compiling: rm *.o; ghc -fglasgow-exts -ddump-simpl-stats -O9 --make rules.hs

module Main where

main :: IO () main = do print $ test 0 print $ test2 0 print $ testRewrite 0 print $ testRewriteReverse 0 print $ testRewrite2 0 print $ testRewriteReverse2 0

test :: a → Bool test x = pi where f = replicate 2000 x i = repeat x pf = lenGT f 300 pi = lenGT i 300

test2 :: a → (Bool,Bool) test2 x = (pf,pi) where f = replicate 2000 x i = repeat x pf = lenGT f 300 pi = lenGT i 300

testRewrite :: a → Bool testRewrite x = pi where f = replicate 2000 x i = repeat x lf = length f li = length i pf = lf > 300 pi = li > 300

testRewriteReverse :: a → Bool testRewriteReverse x = pi where f = replicate 2000 x i = repeat x lf = length f li = length i pf = 300 <= lf pi = 300 <= li

testRewrite2 :: a → (Bool,Bool) testRewrite2 x = (pf,pi) where f = replicate 2000 x i = repeat x lf = length f li = length i pf = lf > 300 pi = li > 300

testRewriteReverse2 :: a → (Bool,Bool) testRewriteReverse2 x = (pf,pi) where f = replicate 2000 x i = repeat x lf = length f li = length i pf = 300 <= lf pi = 300 <= li

lengthOP :: (Num a, Ord a) ⇒ Bool → (a → a → Bool) → [b] → a → Bool lengthOP v (⊜) [] n = 0 ⊜ n lengthOP v (⊜) xxs n = co xxs 0 where co (_:xs) c | n > c = co xs (c+1) | otherwise = v co [] c = c ⊜ n

lenEQ = lengthOP False (==) lenLT = lengthOP False (<) lenLE = lengthOP False (<=) lenGT = lengthOP True (>) lenGE = lengthOP True (>=)

{-# RULES -- | length "lenEQ_LHS" forall xs n. (length xs) == n = lenEQ xs n "lenLT_LHS" forall xs n. (length xs) < n = lenLT xs n "lenLE_LHS" forall xs n. (length xs) <= n = lenLE xs n "lenGT_LHS" forall xs n. (length xs) > n = lenGT xs n "lenGE_LHS" forall xs n. (length xs) >= n = lenGE xs n

"lenEQ_RHS" forall xs n. n == (length xs) = lenEQ xs n "lenLT_RHS" forall xs n. n < (length xs) = lenGE xs n "lenLE_RHS" forall xs n. n <= (length xs) = lenGT xs n "lenGT_RHS" forall xs n. n > (length xs) = lenLE xs n "lenGE_RHS" forall xs n. n >= (length xs) = lenLT xs n #-}

Best Regards, Cetin Sert

2008/12/18 Luke Palmer

...

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.

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)

Luke

2008/12/18 Cetin Sert

...

Hi *^o^*,

With the following rewrite rules:

lengthOP :: (Num a, Ord a) ⇒ Bool → (a → a → Bool) → [b] → a → Bool lengthOP v (⊜) [] n = 0 ⊜ n lengthOP v (⊜) xxs n = co xxs 0 where co [] c = c ⊜ n co (_:xs) c | n > c = co xs (c+1) | otherwise = v

lenEQ = lengthOP False (==) lenLT = lengthOP False (<) lenLE = lengthOP False (<=) lenGT = lengthOP True (>) lenGE = lengthOP True (>=)

{-# RULES -- | length "lenEQ_LHS" forall xs n. (length xs) == n = lenEQ xs n "lenLT_LHS" forall xs n. (length xs) < n = lenLT xs n "lenLE_LHS" forall xs n. (length xs) <= n = lenLE xs n "lenGT_LHS" forall xs n. (length xs) > n = lenGT xs n "lenGE_LHS" forall xs n. (length xs) >= n = lenGE xs n

"lenEQ_RHS" forall xs n. n == (length xs) = lenEQ xs n "lenLT_RHS" forall xs n. n < (length xs) = lenGE xs n "lenLE_RHS" forall xs n. n <= (length xs) = lenGT xs n "lenGT_RHS" forall xs n. n > (length xs) = lenLE xs n "lenGE_RHS" forall xs n. n >= (length xs) = lenLT xs n

-- | genericLength "glenEQ_LHS" forall xs n. (genericLength xs) == n = lenEQ xs n "glenLT_LHS" forall xs n. (genericLength xs) < n = lenLT xs n "glenLE_LHS" forall xs n. (genericLength xs) <= n = lenLE xs n "glenGT_LHS" forall xs n. (genericLength xs) > n = lenGT xs n "glenGE_LHS" forall xs n. (genericLength xs) >= n = lenGE xs n

"glenEQ_RHS" forall xs n. n == (genericLength xs) = lenEQ xs n "glenLT_RHS" forall xs n. n < (genericLength xs) = lenGE xs n "glenLE_RHS" forall xs n. n <= (genericLength xs) = lenGT xs n "glenGT_RHS" forall xs n. n > (genericLength xs) = lenLE xs n "glenGE_RHS" forall xs n. n >= (genericLength xs) = lenLT xs n #-}

1) Is there a way to tell where 'length' is mentioned, what is meant is for example 'Prelude.length' or any length that works on lists? 2) How can I avoid the following error messages?

module Main where import Data.List main :: IO Int print $ length (repeat 0) > 200 print $ 200 < length (repeat 0) print $ genericLength (repeat 0) > 200 -- error print $ 200 < genericLength (repeat 0) -- error return 0

########: Could not deduce (Ord i) from the context (Eq i, Num i) arising from a use of `lenEQ' at ######## Possible fix: add (Ord i) to the context of the RULE "glenEQ_LHS" In the expression: lenEQ xs n When checking the transformation rule "glenEQ_LHS"

########: Could not deduce (Ord a) from the context (Eq a, Num a) arising from a use of `lenEQ' at ######## Possible fix: add (Ord a) to the context of the RULE "glenEQ_RHS" In the expression: lenEQ xs n When checking the transformation rule "glenEQ_RHS"

3) What speaks for/against broad usage of such rewrite rules involving list lengths?

Best Regards, Cetin Sert

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

2008/12/18 Luke Palmer :

On Thu, Dec 18, 2008 at 1:53 AM, Cetin Sert wrote:

...

Hi,

I tested the following, why does the rewrite rules not fire when using tuples also in testRewrite2, testRewriteReverse2?

...

testRewrite2 :: a → (Bool,Bool) testRewrite2 x = (pf,pi) where f = replicate 2000 x i = repeat x lf = length f li = length i pf = lf > 300 pi = li > 300

Why would you expect it to? The compiler is free to inline lf and li to discover that the rule applies, but it is also free not to. Applying all applicable rules while maintaining the ability to abstract is undecidable (big surprise). Thus the dependency on compiler cleverness I mentioned...

I'm agreeing with Luke here. It's possible that the compiler decided to inline f and i, and length, and determined that lf == 2000 and li == _|_ Or it could have decided not to inline at all. Or some other possibility. If you specify {-# INLINE lf #-}, do the results change? I suspect they might. -- ryan

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe