[Haskell-cafe] lengthOP rewrite rules

[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 <lrpalmer at gmail.com>

> 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.sert at 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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20081218/60f81a6e/attachment-0001.htm