Re: n+k patterns
Original-Via: uk.ac.nsf; Fri, 1 Nov 91 01:19:12 GMT
Simon says:
This is certainly technically feasible. As it happens, our compiler is set
up so that it is easy to compile any pattern which you can express as a
predicate function ("does it match?") plus an extract-binder function ("tell
me the value of n, given the value of the arg").
The remaining issue is the usual judgement of language complexity vs
expressiveness. Myself, I like it.
Simon
In principle I like the idea of having more powerful pattern matching
constructs in Haskell, but unfortunately there is a problem with this
idea. Well, not just with this idea, but with the present language as
well.
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.
The predicate is then v >= k && (v-k) `rem` c == 0,
and the extract-binder is (v-k) `div` c.
(with suitable applications of fromInteger added).
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
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.
This is even a problem with ordinary n+k patterns, where the
report implies a translation of f (n+1) = e
to something equivalent to
f v = if v >= 1 then (\n -> e) (v-1) else ...
and the definitions of + and - may be such that (v-1)+1 /= v.
In general, there is now way to construct the extract-binder function
without knowing inverses for the operations in the pattern, and inverse
functions are generally not known.
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.
Another related problem:
The report says (3.12.2) "Matching bottom against a refutable pattern
always diverges."
Not necessarily. Suppose in the above example, the user-defined Ord
instance makes >= non-strict. This is another example of unusual
behaviour in user-defined instances giving unexpected semantics.
I think pattern-matching needs a big rethink.
--brian
| From: Tony Davie <[EMAIL PROTECTED]>
| Date: Wed, 30 Oct 91 17:04:28 GMT
|
|
| It seems to me that some of the most useful arithmetic divide and
| conquer algorithms express a function of an integer n in terms of
| the same function applied to n `div` 2. Has any thought been given to
| generalising n+k patterns to c*n+k patterns? If these were allowed we
| would be able to express, for instance, the well known algorithm for
| raising numbers to an integer power by:
|
| x^0 = 1
| x^(2*n) = xn*xn where xn = x^n
| x^(2*n+1) = x * x^(2*n)
Re: n+k patterns
Original-Via: uk.ac.st-and.cs; Fri, 1 Nov 91 09:37:40 GMT Brian says there are two distinct problems with n+k patterns, 1) That laws relating * `div` `rem` + - might not hold. 2) A user defined >= might not be strict giving rise to a match of bottom to a refutable pattern converging. The second one could be 'solved` by changing the operational semantics of n+k patterns so that it didn't include the test. I suppose the reason why it was included was that n+k (usually n+1) patterns are traditionally associated with primitive recursive definitions of functions over the natural numbers rather than the integers. But Haskell doesn't have Nat as a `base` type, (though users could define it --- and then get the benefits of exactly the pattern match they needed). I'm not sure if Haskell even has Int as a base type -- or even Bool. Should a user really be allowed to redefine the operators on these types? The first of the problems above could possibly be solved by disallowing n+k patterns from being overloaded and insisting they be of BUILT-IN type Int. Though come to think of it, Ints don't obey the div,rem,*,+,- laws if an overflow is involved. Which leads me to one final comment. Does the Report say anywhere that an overflow gives rise to an undefined result? Tony
fixity of /
Original-Via: uk.ac.st-and.cs; Fri, 1 Nov 91 09:49:13 GMT It has been pointed out to me by the Yale implementers that the expression a*b/c causes a parse error because / is infix rather than infixl and is of the same precedence (7) as * which IS infixl. Is this an oversight of someone on the committee or are Haskell arithmetic expressions different from those of most other languages on purpose? If so what was the purpose? Tony
Re: n+k patterns
Original-Via: uk.ac.ed.mrcvax; Fri, 1 Nov 91 14:00:30 GMT > | Which leads me to one final comment. Does the Report say anywhere that > | an overflow gives rise to an undefined result? > > Yes it does (though you may not like the answer!). See Section 6.8.1, p56. > > Simon The relevant sentence states: "The results of exception conditions (such as overflow or underflow) on the fixed-precision numeric types are undefined; and implementations may choose error (bottom, semantically), a truncated value, or a special value such as infinity, indefinite, etc" Surely this is unacceptable? It is unavoidable that a program might run on one implementation and fail on another, but is it not a basic principle of the language that two implementations will deliver identical results if they deliver results at all? Ian
Re: n+k patterns
X-Comment1: # X-Comment2: # uk.ac.glasgow.cs has changed to uk.ac.glasgow.dcs # X-Comment3: # If this address does not work please ask your mail# X-Comment4: # administrator to update your NRS & mailer tables. # X-Comment5: # Yes it does (though you may not like the answer!). See Section 6.8.1, p56. Simon | Which leads me to one final comment. Does the Report say anywhere that | an overflow gives rise to an undefined result?
Re: n+k patterns
Original-Via: uk.ac.ed.mrcvax; Fri, 1 Nov 91 10:03:45 GMT | Which leads me to one final comment. Does the Report say anywhere that | an overflow gives rise to an undefined result? | | Tony Good question! I think it should, though I fear the efficiency implications. Ian
Re: n+k patterns
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
