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

- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request
- n+k patterns Lennart Augustsson
- Re: n+k patterns wadler
- Re: n+k patterns kff
- Re: n+k patterns Lennart Augustsson
- Re: n+k patterns smk