On Sat, Mar 14, 2015 at 3:53 PM, Matt Oliveri <[email protected]> wrote:
> On Sat, Mar 14, 2015 at 1:23 PM, Jonathan S. Shapiro <[email protected]> > wrote: > > The reason it is incomplete is > > that you have omitted the effect type variables on the arrows. Once those > > are restored, the necessary identities will once again be preserved. > > You didn't say anything about an effect variable, you trickster! :) > > > I can't write this using your notation, because the afn notation doesn't > say > > what I need. I think the *correct* substitution of an abstract function > type > > here would be to substitute > > > > 'a -a1-> 'b -a2-> 'c => 'r > > > > for the 'a parameter type in my typing of choose_one. By unmasking the > > effect variables, it becomes clear that all of the arities have to go in > > positionally correlated ways. > > Well I suppose that would take care of it, but are those really > effects? It seems like it's really just answering "Function type > really here? y/n" Saying between which argument types there is a cfn > is _exactly_ what an afn's deep arity does. > So no, I agree, these aren't really effects, or at least they don't behave the same. They are effect-like in the sense that there is a property bound to the arrow that we need to deal with in the checker. In a much weaker sense, they are effect-like in the sense that if your checker or inference engine already needs to deal with effects then there is a natural place in the implementation to deal with this as well. I've been trying to pin down what the difference actually is, though. In essence, I think it's the fact that we aren't dealing with a subtype relation. So (e.g.) if we had three functions nh1 ha2 nh3 (nh: no heap, ha: heap allocating), we would generally say that choose_one nh1 ha2 nh3 is a legal call. The three types meet on the return type in the usual way for subtypes, using an inequality constraint, with the result that the return type is *potentially* allocating. The thing about inequality constraints is that they are only weakly bidirectional; unless we get some further constraint on the return type, no change will back-propagate into the types of nh1, ha2, nh3. Or rather, an inequality constraint propagates, but is immediately statisfied by the pre-existing "allocation types". By contrast, the "this arrow is really a call arrow" is not a subtyping issue. Either the call happens, or it doesn't. It's an equality constraint rather than an inequality constraint. I've attached a short table showing how your (mixed arrow with > "effect" variables) type above does the same thing as (afn 'ar 'a 'b > 'c=>'r). I looked at your table. It appears to me that we are encoding the same things in different ways, and that either will work. It also looks to me like we share a common awkwardness in our encodings. There are actually three "values" that the variable on an arrow can take on (I'll call this variable a "callvar" below) not-yet-bound is-a-return-point not-a-return-point In my case, the discussion where I introduced the => arrow was talking about abstract arrow types, In such types, the is-not-a-return-point case doesn't arise, because we haven't introduced concrete arities yet. In *both* of our notations (I think), the consequence of writing "cfn" is that it fixes any remaining unbound callvar to not-a-return-point. I don't object to the mixed notation; I'm merely noting that it's a bit unusual. In any case: Unless there is a reason to prefer the afn notation that I may not be seeing, I think I would prefer to pursue this using the effect-like variable approach. I don't think it's a better (or worse) encoding, but I think that writing type rules in the callvar style may be clearer (if only to me). Is there something else here that I may be missing? shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
