Re: Lisp pattern matching libraries & difference between unification and pattern matching

On Jan 28, 9:26 am, Jon Harrop <use...@xxxxxxxxxxxxxx> wrote:
Don Geddis wrote:
Marco Antoniotti <marc...@xxxxxxxxx> wrote on Sat, 26 Jan 2008:
To a first approximation, unification is a generalization of pattern
matching.

Actually one must differentiate between two forms of "pattern matching"..
The term as used in conjunction with regular expressions denotes a
slightly
different version than the one used in "structure matching".  This last
one is also used heavily in the ML-style languages.

OK, but it's still the case that unification is a generalization of that
form of pattern matching also.

In a practical sense, ML style pattern matching is designed to integrate
into the type system in a way that unification cannot.

Consider translating the following trivial OCaml pattern into
cl-unification, for example:

# let f (`A x | `B x) = x;;
val f : [< `A of 'a | `B of 'a ] -> 'a = <fun>

This is completely off as you are confusing levels of interpretation.
Deep down in OCaml there is a unification algorithm (unless some magic
has happened since Hindley and Milner). CL-UNIFICATION works at that
level. Your example is at the language level and CL-UNIFICATION will
take care of that, provided that the appropriate semantic rules are in
place in a mostly S-expr syntax that may, or may not, be a
representation of CL.

Your example is at the level of saying that you cannot write
invertible predicates in Ocaml while trying to set up a Prolog system.

While CL-UNIFICATION gives you bits and pieces that resemble ML-like
languages, that is done mostly for convenience and showing off :) It
is a constituent, though not a replacement (although one could
conceive one) for a full blown type-inference machinery based on HM
ideas.

Cheers
--
Marco

.

Relevant Pages