On Mon, 2006-09-04 at 09:33 -0400, Jacques Carette wrote:
> skaller wrote:
> > ---------------------------------------------
> > // THIS DOES NOT WORK because unconstrained
> > // pattern matching is NOT confluent
> >
> > typedef fun ite(b:TYPE, s:TYPE, r:TYPE): TYPE =>
> > typecase [] True =>
> > typecase [x] x => s endcase
> > endcase
> > b r
> > ;
> >
> The issue here is that if b is a "free variable" (representing a TYPE),
> then you don't know what b might be specialized to. It might be a
> constructor, it might be 'x' (or contain it), it might be lots of
> things, all of which will cause things to go wrong.
>
> So your ite function should not evaluate until it has actual parameters
> [if I understood your explanation correctly].
Right, so translating that, the parameters b,s,r have to be substituted
into the body of the function *before* it is reduced.
With my typematch reduction this is not necessary, instead
of there being a constraint on when the reduction can be
applied, the reduction is universal is the identity
in the case the constraint applies (in other words,
the term doesn't get reduced .. :)
However my statement is based on an unproven assumption,
that is if the argument and pattern unify, it is always safe
to attempt a reduction. Even if it is premature and the match
succeeds, subsequent substitutions simply compose with the
result and lead to the same answer.
For example if we did a match:
| x => ctor + b
where x is a pattern variable, it doesn't matter if b is replaced
before or after the match. I think this is obvious for the RHS,
but for the pattern it may be wrong, eg something like
match a + b with
| z+c => ... // z pattern variable
The pattern unifies with the argument: z/a, c/b, but the match fails
because c isn't a pattern variable, and c!=b. After substitution
such as c/b however it will match.
This cannot happen with my original typematch, because the
patterns had to be constants: every symbol was either a pattern
variable or constructor, no 'free variables' into which you could
substitute.
With patterns being expressions admitting substitutions,
this isn't so. However provided the substitutions are
done first, before pattern matching, the problem must go
away.
this basically suggests what Peter said is right: the body of
a lambda or RHS of a case must NOT be reduced until after
the match is done and the resulting substitution applied to it.
the current algorithm reduces the RHS eagerly, before attempting
to apply the binding, then again afterwards .. so it seems lazy
evaluation is mandatory.
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
Felix-language mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/felix-language
