Original-Via: uk.ac.nsf; Tue, 5 Nov 91 21:31:13 GMT
Original-Sender: [EMAIL PROTECTED]

Mark says:

        This problem isn't just restricted to pattern matching ...

I'm interested in the assumptions that an implementation can legitimately
make about the way overloaded functions behave. Other non-standard
behaviour will affect the readability of the program, but will not give
rise to complaints about compiler error. E.g.

          o  n + 0  =  n
             n * 1  =  n
             If these properties don't hold, functions like sum, product,
             genericLength and so forth are going to give peculiar results.

This, with most of the other examples, is a user's problem, because the
system defined types behave sensibly. 

          o  Equality should be symmetric and transitive.  Otherwise you're going
             to start wondering whether  f 0 = 1;  f n = n * f (n-1)  is interpreted
             as          f n = if n==0 then 1 else n * f (n-1)
             or          f n = if 0==n then 1 else n * f (n-1)

This is good example. Should the Report state how implementations are to
translate matching of constant patterns? Or should it state that
implementations are free to assume symmetry here?

        As in Brian's message, none of these properties can, in
general, be guaranteed
        for arbitrary user-defined instances of a particular class:

        | While these hold for built-in types, there is no guarantee they hold for
        | all user-defined types with Integral instances, where the user is free to
        | define the various overloaded class operators IN ANY WAY WHATSOEVER.

        Does this mean we have to throw out the facilities for
arbitrary user-defined
        instances?  Absolutely not!

Indeed, but we do need to state what properties implementations may
assume, and while this is reasonable for small extensions to the language,
it may become a problem for larger ones. My message was prompted more by
Simon's response than by Tony's proposal.

        Personally, I favour an approach to programming with overloaded values
        in which each class declaration is accompanied by a number of laws which
        the operators of that class are expected to satisfy, and each instance
        declaration is accompanied by a `proof' that those laws are indeed
        satisfied for the particular instance involved.

        In reality, I would not expect most programmers to construct suitable
        proofs and it seems unreasonable to expect that the machines will (in
        general) be able to generate the proofs automatically.  One compromise that
        might be worth considering is to extend the syntax of class declarations
        to include laws as part of the concrete syntax.  This would have two
          a) the designer of a particular class has an opportunity to indicate
             his intentions about the way overloaded symbols behave, formally
             as part of the program.
          b) the Haskell type checker can be used to ensure that the stated laws
             are at least type safe.

I agree. I'd like to see a discussion of this on this list.

        | Tony wants a c*n+k pattern to match a value v such that
        | v = c*n+k for some n >= 0, and then to bind n to (v-k) `div` c.
        | ...
        | For this to work sensibly, some laws must hold, e.g.
        | (c * n) `div` c = n  
        | (x `div` y) * y + (x `rem` y) = x
        | (n+k) - k = n

        I don't think these laws are particularly unreasonable...

Nor I. But since they may not hold, implementations need to have the
approval of the Report before assuming them.


PS I've been running Gofer here, and may use it for teaching next year, at
least until the new Haskell implemetations appear, so please add me to
your list of users (at both addresses).

Brian Boutel,
Usually [EMAIL PROTECTED], but currently [EMAIL PROTECTED]
Phone (203) 432 1289

Reply via email to