Original-Via: uk.ac.ox.prg; Fri, 1 Nov 91 18:04:12 GMT Brian Boutel writes: | With Haskell as it is currently defined, one can take an operational view, | that the syntactic translation given in the report defines the semantics | of n+k patterns, and too bad if the semantics of the introduced functions | are not what was expected. I suppose it would be possible to extend this | to other forms such as c*n+k patterns, but again givng specific | translations, but to generalise would require the compiler to assume | semantic properties of operators in order to derive inverse functions for | the extract-binder functions. This problem isn't just restricted to pattern matching ... After all, most Haskell programmers are going to expect certain properties of overloaded operator, regardless of the instances at which they are used: o Addition (+) and multiplication (*) are commutative. In addition, the standard prelude fixity declarations for these operators rely on an implicit assumption that they are associative. 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. 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) o Reading the string representation of a value of type in class Text which was originally produced by show, really ought to give the same value back (i.e. read . show = id) otherwise we cannot guarantee being able to write programs which store data in text files to be read back by other programs some time later. o All kinds of other familiar properties for other familiar operators... 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! 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. | 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... Incidentally, I'd suggest that we have separate (c*n) and (n+k) forms of pattern ... extending the syntax of patterns to: pat ::= .... | int * pat | pat + k This would allow c*n+k patterns as a special case, but also permits other potentially useful constructions: (2*_+1). Even a pattern like (n,m)+1 would make sense if you had an instance of the form Integral (a,b). What's more, using the two forms of pattern seems to give a cleaner system (I've just added it to Gofer and it seems fairly straightforward). Mark

- 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
- Re: n+k patterns haskell-request
- Re: n+k patterns haskell-request