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
benefits:
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.
--brian
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
