On Fri, Mar 27, 2015 at 7:37 PM, Matt Oliveri <[email protected]> wrote:
> On Fri, Mar 27, 2015 at 10:48 AM, Jonathan S. Shapiro <[email protected]> > wrote: > > > OK. On to Matt's concern. In essence, it seems to be that we have two > > parameters that cannot specialize independently. So when we see: > > > > 'a->...->'b-?r->'c > > > > we can specialize that '?r' to 'y' only if we know that 'c is not a > function > > type (which therefore might introduce more arrows on the right). > > That's not what I was saying. It's that we can only specialize ?r to n > if we know that 'c _is_ a function type. I don't think there'd be any > situation where we can't specialize to y. Thanks for saying it again. So I agree that in principle this is awkward, but I'm not convinced that it arises in practice. First, the only inference scenario where we might be tempted to infer something like 'a->'b->'c is in the context of an application like f a b but in that context the correctly inferred type would be 'a -?-> 'b -y-> 'c. More generally: in the scheme that I have been outlining it is *intentionally* true that specializations from ?r to 'y' occur through a different mechanism than specializations from ?r to 'n'. Basically: applications can cause a specialization from ?r to 'y', and specializations to cfns can induce specializations from ?r to 'n'. In the ?r to 'y' case, as you note, the specialization can always be safely be performed (though it may result in a later type incompatibility). In the ?r to 'n' case, the fact that this specialization can only arise from specialization via a cfn means (because cfns always have an explicit return arrow) that the specialization can only occur in contexts where doing so is correct. This is exactly why I originally described arrows as having only the ?r and 'y' options, and not the 'n' option. Eliminating the 'n' from the arrow type syntax means that it's impossible to introduce an incorrect arrow type even by hand. Allowing them to be specialized by cfns INTO cfns has the effect that n-ary calls get introduced in a structured way, without the risk of 'n' appearing in the wrong place. > > Another way of saying this is that we have a type rule that is partially > > type-driven rather than purely syntax driven. Something like (warning: > > unicode characters follow): > > > > Γ ⊢ t1 -?r-> t2 Γ ⊢ t2 :: NonFunctionKind > > ---------------------------------------------------------- > > t1 -y-> t2 > > > > That is: the moment we know the result type is not a function we are > allowed > > to fix the ?r to 'y'. > > So of course that rule would have to be a little different to try to > capture the restriction I was talking about. > Yes. Actually, the mere existence of this rule more or less demonstrates the need for AFN types, because it's too general. It also prompts me to realize once again that I have continued to indulge in confusion about the type 'a->'b->'c in that I continue to think about it as (essentially) afn 'a 'b -> 'c > > Aside from the fact that I've probably boogered the > > writing of the rule somehow, the real problem is that it isn't really > syntax > > driven. It's very much like an implicit coercion that way. > > I don't know what you mean. What's "syntax driven"? Is that the same > as syntax-directed? Yes. I probably should have written syntax-directed. It matters because this rule (as I have written it) doesn't get applied according to the inductive structure imposed by constructions. It inadvertently introduces bounded but nondeterministic search into the type inference process, which isn't a good thing. I think the right thing to do for now is to write using AFN, and then we can go back later and figure out if a notation more similar to ML and Haskell conventions is pragmatically tolerable. In order to discriminate your afns from mine in our discussion, I propose that you write the arity type variable as ?r rather than 'r. > > The problem that > > this rule introduces is a problem of convergence; we need to confirm > that if > > two type rules modify this arrow, they do so with the same result. > > So you mean we need to be sure that the same type doesn't get > instantiated in incompatible ways in different places? But I figure > what you're saying with that rule is that we can only instantiate the > callvar a certain way once we know enough about the return type. So > how would that happen? > I don't think that it *is* possible. But if we are looking at 'a -?r->('b :: non-function) its possible that we can unify something (on the one hand) or apply the arrow promotion (on the other). At that point we have a divergent search happening, and it's important that all paths through the rewriting graph end up with the same answer. > > > I provisionally think that the problem of non-independent type variables > > applies to afn types as well. When I specialize the argument type > variables, > > I have to update the arity type variable as well. Perhaps Matt can > explain > > to me why that isn't an issue? > > I don't see why type variables in the argument types would affect > anything. I am not trying to make tuplized arguments and multiple > arguments look the same, if that's what you're thinking. (That might > not be a bad idea, but I haven't been thinking about it at all.) > > Can you give an example where an argument type affects the arity of a > function in any way? I'm not sure, but let me try. The difference between an AFN and a CFN is that the AFN does not say *how* the arguments must be consumed. So in particular, it's reasonable to rewrite (through unification) afn ?r 'a 'b -> 'c with afn ?r1 'a -> afn ?r2 'b -> 'c in which the arities have degenerated to '1' because each afn accepts just one argument and the arity is therefore known. The point here is that the rewrite has to update a bunch of variables in a consistent way rather than updating just one at a time. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
