[GHC] #10804: Rules conditional on strictess properties

[GHC]

#10804: Rules conditional on strictess properties
-------------------------------------+-------------------------------------
              Reporter:  nomeata     |             Owner:
                  Type:  feature     |            Status:  new
  request                            |
              Priority:  low         |         Milestone:
             Component:  Compiler    |           Version:  7.10.2
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 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.

 {{{#!hs
 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

 {{{#!hs
 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:

 {{{#!hs
 {-# 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10804>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler