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. 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. 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 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". shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
