Marcin 'Qrczak' Kowalczyk wrote:
> How would you define the semantics of matching on functions? This is
> like computing the inverse of arbitrary functions or solving arbitrary
> equations! For example,
I think a limmited form of function pattern mathing could be introduced in the form of
lambda patterns. This would be just a syntactic sugar for a let expression. Programs
would
have to be `desugared ' prior to transforming pattern mathing to case expressions.
Consider
a queue implementation via catenable lists of the type [a] -> [a].
head (\s-> x : xs) = x
tail (\s -> x : xs) = \s -> xs
snoc (\s -> xs) = \s -> x : xs
which would be equivalent to
head q = let (x : xs) = q x in x
tail q = \s -> (let (x : xs) = q s in xs)
snoc q = \s -> (let xs = q s in x : xs)
The additional benefit of this approach would be easier optimization: unique (unshared)
functions could than easily be compiled into direct graph update. This way we can
implement
data structures with pointers to various parts of the object as functions with
appropriate
number of arguments. Functional update would be just pointer update (this direct
functional
update can, of course, be implemented without ``lambda pattern mathing'', but I think
they
fit together well).
I think I managed to define a precise semantics for lambda pattern mathing. Basicly it
amounts to replacing lambda pattern (\s->e) on LHS with a variable q and then replacing
occurence of part e1 of lambda body e with ``let e = q s in e''. From this we conclude
that
variable s in a lambda pattern has to be bound on RHS. We could inforce this by
putting the
whole RHS in a let expression:
RHS': let s = error in RHS
This can be expanded to the case of (\p -> e) pattern where p is a pattern (with zero
or
more free variables).
As another example, the definition of join for state transformer monad becomes
join (\s -> (\s' -> (x, s''), s')) = \s -> (x, s'')
which after performing transformation and some simplifications, becomes
join q = \s -> (let (u, s') = qs
(x, s'') = u s'
in (x, s''))
I stress that this is just a syntactic sugar. There is no way we can tell the way the
argument function was defined by this pattern mathing, as it always succeeds (being
replaced by a type variable).
