[Haskell-cafe] lengthOP rewrite rules

[Cetin Sert]

oh, btw I am using GHC 6.10.1 (on Linux x86_64)

2008/12/18 Cetin Sert <cetin.sert at gmail.com>

> 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/5b99c0fc/attachment.htm