[Haskell-cafe] Preconditions as Typeclasses (Was: Re: Mysterious factorial)

[Luke Palmer]

On Wed, Dec 30, 2009 at 11:15 AM, Ralf Hinze <ralf.hinze at comlab.ox.ac.uk> wrote:
>> I would use:
>>
>> foldm :: Monoid m => [m] -> m
>>
>> Which is just a better implementation of mconcat / fold.  The reason I
>> prefer this interface is that foldm has a precondition in order to
>> have a simple semantics: the operator you're giving it has to be
>> associative.  I like to use typeclasses to express laws.
>
> That's a valid point. Unfortunately, Haskell is not Coq, so there
> is no guarantee that the monoid laws are actually satisfied. And
> using a type-class has the downside that you can have only one
> instance per type. Maybe, you want to use both `foldm (+) 0' and
> `foldm (*) 1'. So the bottom-line is that you should have both
> versions.

Well, it's a matter of taste, which I'm trying to argue into
convention  (eg.
http://lukepalmer.wordpress.com/2009/07/01/on-the-by-functions/ ).  I
mean, if you can do foldm (+) 0, it seems quite reasonable to be able
to do foldm (-) 0.  However, given:

newtype Sum a = Sum a
instance (Num a) => Monoid (Sum a) where
    -- (+) is associative with 0 as its identity
    mempty = Sum 0
    mappend (Sum a) (Sum b) = Sum (a + b)

It is not so obvious that you can do:

newtype Difference a = Difference a
instance (Num a) => Monoid (Difference a) where
    -- (-) is associative with 0 as its identity NOT
    mempty = Difference 0
    mappend (Difference a) (Difference b) = Difference (a - b)

Admittedly it is quite a lot more typing, and I do like brevity, but I
also like unverified preconditions to be very loud.  Once the tech is
there, I would like to require a *proof*, but since proving is still
hard and Haskell has no support for it, I need some way to document
preconditions.  I really like that knowing the name and type of a
function is enough to use it most of the time, so documentation isn't
really a good place for such preconditions.  Typeclasses already have
the habit of coming with laws, so I take it to the extreme and encode
all my preconditions in typeclasses.

It is less convenient.  But preconditions that are not verified by the
typechecker are rare in Haskell code, and proofs of preconditions are
subtle, so let's encourage abstraction and documentation of such
proofs.  In all places except  instances, let's be certain that the
typechecker does all of our verification work.

Luke