Opened 4 years ago

Last modified 4 years ago

#10804 new feature request

Rules conditional on strictess properties

Reported by: nomeata Owned by:
Priority: low Milestone:
Component: Compiler Version: 7.10.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Runtime performance bug Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (1)

comment:1 Changed 4 years ago by thomie

Type of failure: None/UnknownRuntime performance bug

These tickets are related to runtime performance.

Note: See TracTickets for help on using tickets.