On Tue, Feb 24, 2015 at 6:31 PM, Matt Oliveri <[email protected]> wrote:
> This helps, I think, but I still don't fully understand. > > On Tue, Feb 24, 2015 at 7:47 PM, Jonathan S. Shapiro <[email protected]> > wrote: > >> > Rewriting this using the full (unelided) notation, we would be > >> > specializing > >> > fn arity a->b->c->d->r > >> > > >> > with > >> > fn 2 a b -> fn newarity c->d->r > >> > >> Yeah, I got all that. But I don't understand it. Maybe you're not > >> seeing which subtlety is tripping me up. I figure an abstract type is > >> instantiated to something concrete by plugging in concrete elements of > >> the appropriate kind for the variables. Well let's simplify the > >> example, and say a, b, c, d, and r are metavariables for concrete > >> types, and r is not a function type. Then (fn arity a->b->c->d->r) is > >> abstract because it has one variable, of kind Nat. Not all nats are > >> legal instantiations, just 1, 2, 3, or 4. So by naive reasoning, that > >> type has four concrete instances. > > > > I agree. > > So maybe I'm confused about terminology. In terms of implicit > quantifiers, and the logical operation of universal instantiation, it > has four instances, unless I'm doing the implicit quantifiers wrong. > I think that depends on whether we are doing shallow or deep specialization. I have been talking exclusively in terms of shallow specialization. But if (for example) we conclude that the leftmost specialization has arity 1, then there remain three argument positions to concretize. Those can be concretized as [1, 1, 1], [1, 2], [2, 1], or [3]. If I am not mistaken, Keeans' enumeration of possible arities is intended to be a deep enumeration. I think he's mistaken, because the return type 'r can unify with a function type and thereby extend the arities. But assuming that does not occur, his enumeration seems reasonable. > > So in my example above, we specialized > > > >> fn 'arity 'a->'b->'c->'c->'r (label this type T1) > > > > > > with (renaming vars) > > > >> fn 2 'v 'w -> fn 'newArity 'x->'y->'z (label this type T2) > > > > > > Because the return type in T2 is abstract, the type resulting from > > specializing T1 remains abstract. > > Yeah yeah. I understand just fine why it _should_ work that way. I > just don't see what formal rules actually make it work that way. > I haven't tried to write the formal rules, but it follows from the axiom of choice. I agree that we need to capture formal rules for this. > > Note that the only way the return type of T2 can be abstract is if 'v or > 'w > > is abstract. > > You mean the (fn 'newArity ...) part? That can't be right. Remember, I > wanted a, b, c, d, and r to be concrete types. I'm only mildly irked > if you change the names of my metavariables, but if you say v or w > (were a and b) to be abstract, then you're not using my example. > So: I agree that I moved the example, though it was through misunderstanding rather than nefarious intent. :-) Unfortunately, if I stick to your example, the unification we are trying to consider becomes impossible. Let me stick with my variable names to avoid confusion between the abstract and the concrete types we are discussing. If the types at 'v 'w 'x 'y (the argument positions on T2) have concrete arity, and the arity of tn in T2 is concrete, then it follows that if the return type of T2 is a function type, it is necessarily a function type having concrete arity. If that is so, then any leftmost unification with 'a->'b->'c->'d->'r necessarily yields a concrete return function type. > > In that case, it will turn out that 'newArity was introduced by > > one of the types at 'v or 'w. The "new" arity type variable didn't > actually > > appear from nowhere. The mildly puzzling part is to explain coherently > how > > and why it ends up where it does in the result. > > I don't see how, since 'v and 'w are argument types, and 'newArity is > in the return type. > Reasoning: fn itself has concrete arity. Any local procedure constructed inside fn (transitively) has concrete arity, because we can see the definition. If such a function is returned, then the result type is necessarily concrete. If f itself is returned then the result type is fn, which is concrete. Any concrete global slot of function type has concrete arity. If the value in such a slot is returned, the result type of fn will have concrete arity. The only remaining source of arity-abstractness comes from the arguments. > It seems to me that I made a mistake in my description, however. It seems > to > > me that I should have spoken about unification rather than > specialization. > > Which description are you referring to? > I keep referring to this as specialization, and on reflection I think I should be saying unification. > Well intuitively, we don't need the shallow arity either. We could > just have separate constructors for arity-abstract function types and > arity-concrete ones. That would correspond to the notation that I started with. The choose_one example made it clear that we needed a way to do unification over arities. Syntactic clarity and consistency in our discussion then suggested having a position describing arity in all fn types. Personally, I find "fn 'a 'b -> 'c" more readable. But in the present discussion it is helpful to have a single consistent notation to avoid the confusion we have already incurred. For the sake of regularizing our discussion, I'm asking that we **for now** use the syntax "fn 2 'a->'b->'c". Later we can introduce convenience syntax, but for the moment it is very helpful to be explicit for the sake of a clear discussion. > But choose_one shows that that doesn't actually > work. What makes you think that choose_one-like problems are happy if > only the shallow arity can be constrained? > Perhaps the fact that I didn't say that. The thing is: when the shallow arity is constrained, that newly introduced type variable for the remaining arity specializations is introduced, and it is required to specialize in the same way for all of the choose_one arguments, because they all have the same type. So in one sense, only the shallow arity is constrained. But the introduction of a commonly referenced 'newArity ensures that (a) deep arity is constrained only by syntactic compatibility, but (b) all arguments of choose_one must specializa in the same way w.r.t. arity. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
