On 31 March 2015 at 21:28, Jonathan S. Shapiro <[email protected]> wrote:
> Keean: > > You seem to misunderstand the challenge problem. > Its definitely possible, i'm not convinced yet. If there is an issue, I don't fully understand it. > > 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. > Just ignore that, it doesn't make any different to my argument, it just means where I list the possible types of the imported 'f' we would use 'a -> b -> c -> d' for a local (arity abstract) definition, or if you prefer, put the concrete calls at the positions you want to infer them from the lambdas in the definition. > > 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. > I think I have demonstrated how it can be handled without. I would appreciate if you could find the problem with what I have suggested. It seems to work for me. 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) > Sorry, I just missed one argument so I have a->b and a->b->c->d, I don't think this changes any of the arguments. > 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. > You don't need the intersection types, that was before I worked out the unification algorithm I posted, which is commutative (IE unifying a and b then c is the same as a then c then b). > > That said, intersection types may be a more natural way to think about > things in a type system that admits subtypes. > True, however they do nasty things to unification, and you have to introduce expansion types. I've been down this road quite a long way, and I didn't like it. Top level intersections are fine though, but not necessary. The imported type of 'f' must unify with both of these, so valid types >> would be: >> > > F is not imported. > Again, whether f is imported or not is not relevant to my argument, so you can ignore that and read 'type inferred from the definition' instead of 'type defined in the import/export'. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
