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 <cetin.s...@gmail.com> > 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 > >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe