There is a problem in Felix with constraint propagation .. well the
problem is that constraints are NOT propagated. Consider:
fun f[u where u in ints] (x:u) => f(x); // fails
Here, the argument to f on the RHS is x, which has type u,
but the type has to be a member of the set of ints, which
a general type variable is not.
It would seem that the constraint "in ints" should be propagated,
which could be done if the type of x was "u | u in ints" but
the type is just u. The constraint "in ints" is checked on a call
to f, so that
f 1; // passes
f 1.0; // fails
but then the constraint is forgotten: it isn't part of the type.
The problem here is shown by a more general case:
fun g[u,v where H(u,v)] (x:u, y:v) ..
where H is some predicate of two variables.
For example
H(u,v) : u = int * v
In which, the constraint isn't a property of a single
variable but a relation between them. Now it is
very much harder to check if a call like:
z = y;
g((1,&y),&z)
conforms to the constraint: at least, this requires
constraint unification (actually, specialisation),
and probably a general prover. For example
fun h[u,v where X(u) and Y(v)] (x:u, y:v)
fun k(u,v where Y(v) and Xu)] (x:u, y:v) => h(x,y)
satisfies, but you have to know that "and" is
symmetrical to derive this.
The general problem is: given
fun a[u1, u2 .. where H(u1, u2 ..)]
(x1:P1(u1, u2, ..),x2(P2(u1,u2 ..), ..)
..
b(y1,y2...)
fun b[v1, v2, .. where J(v1, v2) ..]
(y1:R1(v1,v2..), y2 ... )
where
typeof y1 = Q1(u1, u2 ..
typeof y2 = Q2(u1, u2 ..
..
we have to prove
Q1 = R1
Q2 = R2
..
and
H implies J
The first part is proven by overload resolution using
specialisation (directed unification): this is "easy"
because it is just a set of type equations.
In fact the second part is ALSO a type equation,
but it may at least involve operators like "and"
which is an intersection which as noted cannot
be done just using unification, because the obvious
example:
r and s = s and r
won't unify, but is equal anyhow since "and" is symmetrical.
Ditto for "or". note that Felix typematch has a similar problem:
it only works if it can be instantiated with concrete terms
and then reduced, reduction with polymorphic terms
will usually fail.
--
john skaller
skal...@users.sourceforge.net
------------------------------------------------------------------------------
Crystal Reports - New Free Runtime and 30 Day Trial
Check out the new simplified licensing option that enables
unlimited royalty-free distribution of the report engine
for externally facing server and web deployment.
http://p.sf.net/sfu/businessobjects
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
