On Fri, Mar 27, 2015 at 10:48 AM, Jonathan S. Shapiro <[email protected]> wrote: > I was planning to look over Matt's AFN approach today, but there is > something he said about the arrow idea I have been developing that doesn't > seem right, and it looks to me (at first) as if the afn proposal has the > same problem buried in a different place. > > First, let me deal with one dangling question. Matt asked at one point > whether > > cfn 'a 'b 'c=>'r > 'a-n->'b-n->c-y->'r > > are the same type. It hadn't occurred to me that this was so, but it seems > right. Which is kind of nice, because it means that the rules for combining > these "annotated arrow" types are a bit easier to understand. This hadn't > been apparent to me before, perhaps because I had never written the 'n' > arrows explicitly. > > 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. > I think > Matt's objection is that there is a functional dependency here between ?r > and 'c, and that it has crept into the type rules. Yes, once we agree on the reason for the dependency. :) > 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. > 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? I don't think it matters whether it's syntax-directed or not. If you can come up with a way to express the right restriction on instatiating function types, then what's the problem? (Other than that it still seems way easier to me to use afns.) > 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 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? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
