Matt: I think we're heading towards the same place, but given the case we are looking at here I'm not sure why the afn types need to take an arity variable.
Going back to your example, we are focused on the type of f in: def apply1 f = f 1 2 3 // f :: a->b->c->r def apply2 f = apply1 f 4 5 6 // f :: a->b->c->d->e->f->r In the second case, we agree that we have lost a constraint about the requirement for a concrete call boundary after the third argument. One way to write this might be something like: [[a->b->c]->d->e->f]->r But I do not care for this. It suggests a nesting of groups that isn't actually present. Another way to write this might be: a->b->c=>d->e->f=>r where the => arrows indicate required concrete call boundaries. This is a different (and I think, clearer) way of writing what I was trying to say with the "positional" idea. Given this mixed-arrow notation, we can then look at the remaining -> arrows, for example, the: a->b->c => part of things. We know the result type, and we now need to decide how the three arguments a, b, c will be concretely consumed. The possible transformations are: 1. On the basis of the number of arguments witnessed at some application, we can rewrite a -> arrow as a => arrow. 2. We can instead rewrite something of the form => a->b->...x->y => as => cfn a b ... x y => saying, in effect, that we are committed to consuming all of those arguments in a single concrete call. I'm not sure if this is actually different from what Matt is suggesting with AFNs. I think the key issue is that we need a way to mark where concrete call boundaries are required. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
