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