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