Re: [Haskell-cafe] lengthOP rewrite rules

2008-12-19 Thread Lennart Augustsson 
There is nothing better about terminating more often.  Either your
transformation has the same semantics as the original, in which case
it is correct.  Or your transformation has different sematics than the
original, in which case it's incorrect.

  -- Lennart

On Fri, Dec 19, 2008 at 3:03 AM, wren ng thornton w...@freegeek.org wrote:
 Luke Palmer wrote:

 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.

 And if you want to go that route, then see Data.List.Extras.LazyLength from
 list-extras[1]. Peano integers are quite inefficient, but this library does
 the same transform efficiently.

 [1] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/list-extras


 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)

 Data.List.Extras.LazyLength does have rewrite rules to apply the lazy
 versions in place of Prelude.length where it can. My justification is
 two-fold. First is that for finite lists the semantics are identical but the
 memory behavior is strictly better. Second is that for non-finite lists the
 termination behavior is strictly better.

 It's true that refactoring can disable either point, and that can alter
 semantics in the latter case. Since the module is explicit about having
 these rules, I would say that users should remain aware of the fact that
 they're taking advantage of them or they should use the explicit lengthBound
 or lengthCompare functions instead.

 --
 Live well,
 ~wren
 ___
 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

Re: [Haskell-cafe] lengthOP rewrite rules

2008-12-18 Thread 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 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

Re: [Haskell-cafe] lengthOP rewrite rules

2008-12-18 Thread 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 $ test0
  print $ test2   0
  print $ testRewrite 0
  print $ testRewriteReverse  0
  print $ testRewrite20
  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 lrpal...@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.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

Re: [Haskell-cafe] lengthOP rewrite rules

2008-12-18 Thread Cetin Sert 
oh, btw I am using GHC 6.10.1 (on Linux x86_64)

2008/12/18 Cetin Sert cetin.s...@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 $ test0
   print $ test2   0
   print $ testRewrite 0
   print $ testRewriteReverse  0
   print $ testRewrite20
   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 lrpal...@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.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

Re: [Haskell-cafe] lengthOP rewrite rules

2008-12-18 Thread Luke Palmer 
On Thu, Dec 18, 2008 at 1:53 AM, Cetin Sert cetin.s...@gmail.com wrote:

 Hi,

 I tested the following, why does the rewrite rules not fire when using
tuples also in testRewrite2, testRewriteReverse2?

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


Why would you expect it to?  The compiler is free to inline lf and li to
discover that the rule applies, but it is also free not to.  Applying all
applicable rules while maintaining the ability to abstract is undecidable
(big surprise). Thus the dependency on compiler cleverness I mentioned...

There might be something you can do with rule ordering, make sure it happens
after the inlining phase, but I don't know how to do that offhand.

Luke
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] lengthOP rewrite rules

2008-12-18 Thread Ryan Ingram 
2008/12/18 Luke Palmer lrpal...@gmail.com:
 On Thu, Dec 18, 2008 at 1:53 AM, Cetin Sert cetin.s...@gmail.com wrote:

 Hi,

 I tested the following, why does the rewrite rules not fire when using
 tuples also in testRewrite2, testRewriteReverse2?

 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


 Why would you expect it to?  The compiler is free to inline lf and li to
 discover that the rule applies, but it is also free not to.  Applying all
 applicable rules while maintaining the ability to abstract is undecidable
 (big surprise). Thus the dependency on compiler cleverness I mentioned...

I'm agreeing with Luke here.  It's possible that the compiler decided
to inline f and i, and length, and determined that lf == 2000 and li
== _|_
Or it could have decided not to inline at all.  Or some other possibility.

If you specify {-# INLINE lf #-}, do the results change?  I suspect they might.

  -- ryan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] lengthOP rewrite rules

2008-12-18 Thread wren ng thornton 

Luke Palmer wrote:

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.


And if you want to go that route, then see Data.List.Extras.LazyLength 
from list-extras[1]. Peano integers are quite inefficient, but this 
library does the same transform efficiently.


[1] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/list-extras



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)


Data.List.Extras.LazyLength does have rewrite rules to apply the lazy 
versions in place of Prelude.length where it can. My justification is 
two-fold. First is that for finite lists the semantics are identical but 
the memory behavior is strictly better. Second is that for non-finite 
lists the termination behavior is strictly better.


It's true that refactoring can disable either point, and that can alter 
semantics in the latter case. Since the module is explicit about having 
these rules, I would say that users should remain aware of the fact that 
they're taking advantage of them or they should use the explicit 
lengthBound or lengthCompare functions instead.


--
Live well,
~wren
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] lengthOP rewrite rules

2008-12-17 Thread 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