RULES and type classes

[Duncan Coutts]

On Fri, 2007-03-30 at 17:06 +0100, Neil Mitchell wrote:

> The user has called a function which explicitly annotates which
> classes it requires. The user is completely allowed to write "instance
> Ord a where compare = undefined", and they should have a reasonable
> expectation that unless Ord a => is in the context, Ord is not
> involved.

Sure it's not safe in general for existing classes, but I really want to
say this...

class SmallStrictAtomic a
-- only add your type to this class if the ops are strict and total

instance StrictNum Int
instance StrictNum Char
instance StrictNum Int8
...
instance StrictNum Integer

{-# RULES "strict maximum"
   forall (xs :: SmallStrictAtomic x => [x]).
     maximum xs =  strictMaximum xs
  #-}

This is a whole lot easier and more extensible than adding lots of
SPECIALISE pragmas:

{-# SPECIALISE maximum :: [Int] -> Int #-}
{-# SPECIALISE maximum :: [Char] -> Char #-}
{-# SPECIALISE maximum :: [Int8] -> Int8 #-}
...
{-# SPECIALISE maximum :: [Integer] -> Integer #-}

So yeah, the laws for this class are not checked (and I didn't specify
them either ;-) though of course I should if we want to let other
modules add instances), but it's a class specifically created for the
purpose of taking advantage of those laws so if you worry then don't add
your type to that class. It doesn't silently rewrite existing programs.

More generally I'd like to have ways for programmers to make promises
about properties of their values or types so that optimisation rules
could take advantage of them, ie rules with side conditions where we can
look up and see if the programmer asserts the properties needed to
fulfil the side condition.

Duncan