On Tue, Mar 31, 2015 at 1:18 AM, Jonathan S. Shapiro <[email protected]> wrote: > On Mon, Mar 30, 2015 at 5:54 PM, Matt Oliveri <[email protected]> wrote: >> On Mon, Mar 30, 2015 at 9:59 AM, Jonathan S. Shapiro <[email protected]> >> wrote: >> > The one I'm less convinced about is whether (your afn here) >> > >> > afn ?r1 'a 'b -> afn ?r2 'c -> 'd >> > >> > is equivalent to (your afn) >> > >> > afn (?r1 ++ ?r2) 'a 'b 'c -> 'd >> > >> > the thing that has been lost here is where the first arrow appeared in >> > the call chain. >> >> So this is a bit subtle, and it is a disadvantage, which is why I now >> prefer the mixed arrow-ized afns. If you could write "afn (?r1 ++ ?r2) >> 'a 'b 'c -> 'd" as a user, you're absolutely right that there is no >> intermediate call arrow imposed. But when we write "afn ?r1 'a 'b -> >> afn ?r2 'c -> 'd", it's implicit that ?r1 sums to 2. This is where the >> call arrow is hiding. In the scope of a certain ?r1 and ?r2 with the >> appropriate constraints, (afn (?r1 ++ ?r2) 'a 'b 'c -> 'd) and (afn >> ?r1 'a 'b -> afn ?r2 'c -> 'd) are the same type, even though the >> former way of writing it would not imply that ?r1 sums to 2. > > > Another way to write all this would be to allow something like > > afn 'a 'b -> 'c 'd -> 'ret > > where arrows indicate known callret positions and adjacent variables > indicate positions that may or may not be a callret.
What are you proposing here? A change to deep arity afn notation? I'd rather abandon deep arity entirely, and use (list bool) mixed arrow-ized afns. 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, assuming the elided callvars are the same. (In other words, you need to be convinced that group splitting works.) > Once we've allowed > multiple vars to appear adjacent to each other, we don't really need two > arrows anymore, and the leading "afn" provides a sufficient bracketing. I agree, since at this point we will probably not need to write the analogue of 'n' arrows anymore, except by using cfns. (Oh, one more time. ;) See below.) > This also makes my example above unambiguous: > > afn 'a 'b -> 'c -> 'd > > unifies with > > afn 'a 'b 'c -> 'd > > to give > > afn 'a 'b -> 'c -> 'd I don't know what was ambiguous before, but I agree with this unification. >> I still like to call => a call arrow, since it's _not_ >> known-returning. It can diverge or throw. > > Semantically, BitC models throw by conceptually rewriting all return values > as unions, so that's still a return. I'm not sure what you mean by > "diverge". Infinite loop in a way that doesn't crash, so it really never comes back. But you can model that as "returning" bottom. I don't want to get picky about what "return" should mean, but what I'm saying is that "does-return" seems to be saying something about runtime behavior, but a call arrow is just saying that you syntactically have a return type. In other words, if we had a function (f : 'a-n->'b-y->'c), then (f a) is ill-typed. We cannot call f with one arg. Calling that 'n' "does-not-return" sounds like we can call it and we'll hang forever, which is not at all what we're trying to say. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
