Keean: You seem to misunderstand the challenge problem.
First, f is not imported, so we have no signature for it at all. Assume f is a procedure parameter to the current procedure for which no type is given. We are left to infer an abstract function type for f based on the observed applications in the procedure body. The two applications in the example: f a b f a b c d Occur in the body OF THE SAME PROCEDURE. Thus, the challenge is to infer a single abstract function type for f that satisfies *both* uses simultaneously. You gave inferred types for the two applications independently, but did not account for the need to reconcile them to arrive at a single type for f. Matt and I don't think they reconcile without some ability to remember which argument positions must have a call arrow following the argument position. In particular the choose_one example can't be handled without that. On Tuesday, March 31, 2015, Keean Schupke <[email protected]> wrote: Because I have a multi-set environment we can happily have {f : a -> b, f : > a -> b -> c ->d}, which you could also write using intersection types as f > : (a -> b) & (a -> b -> c -> d) > Those signatures are wrong. You'd need something like F: (a->b->'ret1 ) & (a->b->c->d->'ret2) But introducing intersection types seems like a big increase in complexity in the type system unless we need them for some other purpose. I do agree that this can handle the issue in this example, but there is still a need for some form of arity type variable to ensure agreement in the choose_one example. That said, intersection types may be a more natural way to think about things in a type system that admits subtypes. The imported type of 'f' must unify with both of these, so valid types > would be: > F is not imported. Jonathan
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
