Rules conditional on strictess properties
Hi,
This is taking note of a rough idea, i.e. something that I might want to investigate more deeply some day.
The current libraries contain this code, which makes the compiler switch from foldl
to foldl'
for certain types where min
is known to be strict in the first argument.
minimum :: (Ord a) => [a] -> a
{-# INLINE [1] minimum #-}
minimum [] = errorEmptyList "minimum"
minimum xs = foldl1 min xs
{-# RULES
"minimumInt" minimum = (strictMinimum :: [Int] -> Int);
"minimumInteger" minimum = (strictMinimum :: [Integer] -> Integer)
#-}
strictMinimum :: (Ord a) => [a] -> a
strictMinimum [] = errorEmptyList "minimum"
strictMinimum xs = foldl1' min xs
Is is a bit sad that this can only be done by listing explicit instances. What I would like to see is that it sufficies to write
minimum :: (Ord a) => [a] -> a
{-# INLINE [1] minimum #-}
minimum [] = errorEmptyList "minimum"
minimum xs = foldl1 min xs
and then there are general rules taking care of choosing the right foldl
variant:
{-# RULES
"strict foldl" forall f. mumble_mumble f ==> foldl f = foldl' f
"strict foldl1" forall f. mumble_mumble f ==> foldl1 f = foldl1' f
#-}
The mumble_mumble
would be some way of specifying the required strictness properties of f
, which would be checked use the strictness analyzer. A simple isStrict f
is probably not sufficient (The information that f
is strict in the first argument also depends on how many arguments we pass to f, as min ⊥ ≠ ⊥
, but ∀x. min ⊥ x = ⊥
). Maybe ∀x. min ⊥ x = ⊥
, or some ASCIIfication of it, is indeed the proper sytanx....
This is related to #9137, which also wants conditional rewrite rules with certain compiler-checked aspectes of some of the matched variables.
I think there is also a ticket (or at least an idea) about rewrite rules being conditional on some equation (e.g. (not very useful) RULES forall f (*). (forall x y. x * y ≡ y * x) ==> foldl1 (*) (reverse xs) == foldl (*) xs
). I guess the rather vague #9601 covers that.
Trac metadata
Trac field | Value |
---|---|
Version | 7.10.2 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | low |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |