[Haskell-cafe] lengthOP rewrite rules
Luke Palmer
lrpalmer at gmail.com
Thu Dec 18 03:02:57 EST 2008
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/c10b6081/attachment.htm
More information about the Haskell-Cafe
mailing list