On Tue, Mar 31, 2015 at 9:37 AM, Jonathan S. Shapiro <[email protected]> wrote: > On Mon, Mar 30, 2015 at 10:49 PM, Matt Oliveri <[email protected]> wrote: >> I'd rather abandon deep arity entirely, and use (list bool) mixed >> arrow-ized afns. > > Conceptually I think the mixed arrow notation is the right model, though I'm > not sure how "list bool" gets in to this.
(list bool) was the type used to convey arity information to the mixed arrow-ized version of rawAFN. Each bool is a 'y' or 'n' from your callvar notation, but the surface syntax doesn't need y's or n's. > But I'm not all that happy with > having more arrows running around, so I'm playing with a syntactic > alternative. I like your alternative, as long as you don't get confused if I choose to be explicit about grouping. See below. >> If you're proposing notation for that, then my only >> concern is that we want to distinguish (afn 'a 'b->'c 'd->'ret) and >> (afn 'a 'b->afn 'c 'd->'ret) at least long enough to prove they mean >> the same thing.. > > Hang on. You could mean two things here. I'm saying that those two are > *definitionally* the same, one being a shorthand notation for the other. No, I don't like that. We really have two things if you write it as rawAFN: afn 'a 'b->'c 'd->'ret becomes rawAFN [r1,true,r2] [a,b,c,d] ret afn 'a 'b->afn 'c 'd->'ret becomes rawAFN [r1] [a,b] (rawAFN [r2] [c,d] ret) These types mean the same thing, but they're not definitionally the same. That they are the same is the (list bool) version of group splitting. As with deep arities, we can use this perspective to explain afn unification in terms of instantiating quantifiers. I guess we _could_ say both surface syntaxes are the split rawAFN. I mean it wouldn't hurt. Probably. I dunno. You pick. > The > more interesting question you are raising is: do we need a callvar in this > afn notation? > > The answer, unfortunately, seems to be "yes", because > > afn 'a 'b -> 'c 'd -> 'ret > > is equivalent to 'a->?r1->'b=>'c-?r2->'d=>'ret > > and we need the variables there to ensure that conversions from -> to => > happen in proper agreement. I agree. > I think the variables can be done in list form (as you have them) or in > annotated-arrow form; that's just encoding. Since the surface syntax doesn't seem to need any of the machinery for either deep arities or y/n lists, I suppose we could just have (at most) one variable per afn, and be vague about what exactly its instances are. Internally, we use either a y/n list or a deep arity, whichever seems easier. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
