On Fri, Mar 13, 2015 at 12:57 AM, Jonathan S. Shapiro <[email protected]> wrote: > 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.
Well in this case you're right, the arity variables don't say anything interesting. But in choose_one, multiple afns would use the same 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. Yeah, that looks weird. > 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. This notation is pretty nice. But are there actually multiple arrow types there? For example, would it be parenthesized like this? a->(b->(c=>(d->(e->(f=>r))))) If so, then it seems strange to change the "a->b->c =>" part to "cfn a b c =>", as you propose below. If it would instead be parenthesized like this: (a->(b->c))=>((d->(e->f))=>r) then it seems basically the same as my afn notation, but with the arity variables elided. > 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. This makes sense. > 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. This mixed arrow notation does seem to solve the apply2 problem. But it's not clear how it works for choose_one. For choose_one, we'd want to enforce that multiple "a->b->c =>" groups have your rewrites 1 and 2 above done to them in the same way, to get the same concrete arities. This is what sharing of arity variables effectively does in my afn notation. We could allow notation more like your mixed arrow notation, without arity variables, when each group has a fresh arity variable. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
