On Mon, Mar 30, 2015 at 10:49 PM, Matt Oliveri <[email protected]> wrote:
> On Tue, Mar 31, 2015 at 1:18 AM, Jonathan S. Shapiro <[email protected]> > wrote: > > > 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 don't know if I'm proposing anything. I think I'm just noting that a bunch of notations are possible, and that using an "afn" prefix as part of the type doesn't have to be as awkward as it looks. With the notation above, I was pointing out that afn 'a 'b -> afn 'c 'd -> 'ret could be written afn 'a 'b -> 'c 'd -> 'ret which is a bit more readable and conveys the same information. Note I'm assuming here that all function types are either afn or cfn, so we don't need to concern ourselves with other arrows getting mixed in to this. > 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. But I'm not all that happy with having more arrows running around, so I'm playing with a syntactic alternative. > 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. 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 think the variables can be done in list form (as you have them) or in annotated-arrow form; that's just encoding. > 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.) > That's my thought. >> 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. > Fair enough. I was just curious what you meant. That's a good example. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
