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.


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

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.


        | 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)

Reply via email to