[Haskell-cafe] lengthOP rewrite rules

[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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20081218/14ed1e90/attachment.htm