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
