On Mon, Mar 2, 2015 at 11:01 AM, Jonathan S. Shapiro <[email protected]> wrote: > Aside:
I hope you don't mind if I reply to this, which risks turning into a main branch of the discussion. > Several of you, but mainly Matt, have asked why I keep focusing on the > left-most specialization and trying to proceed inductively. From a types > perspective I agree that this is the wrong thing to do. I have implicitly been wondering that all along. I don't remember actually asking specifically, but I might have. > I think the reason I keep coming back to that is that given an application > > f a b c > > the thing that is going to specialize here is the type of /f/. (I thought you didn't like to use "specialize" in that kind of context.) > Only after > the types unify will we learn the return type of f and be able talk about > the next specialization step. But this is only true in the seemingly-irrelevant sense of the concrete function's return type. No matter how many concrete applications (f a b c) turns into, the return type we care about is simply the type of that expression. We can talk about that right away, if only via a type variable. Indeed, that type variable may be instantiated to a function type, and have its own arity concretize before f's arity does. Or at least it seems like an unnecessary and yucky proof obligation to assume otherwise. This is the sense in which instantiation is not guaranteed to proceed from left to right. > So in this sense specialization proceeds > left-ro-right. But as I have just explained, the successive "uncovering" of return types within the original group is not the whole story. > The problem with this view is that all of these chained specializations > actually happen in parallel, and either they all collectively arrive at a > valid unification of types or they do not. Actually, no they don't happen in parallel, if we're talking about instantiation within a group. What makes you think that? <snarky>Probably that you're using Nat for arity instead of List Nat, which is obviously serial.</snarky> Also, I should point out that if you allow regrouping, then of course this whole explanation is completely screwed. > No new proposition or conclusion here. Just an explanation of why I keep > getting stuck in this way. Shap, for all I know, in your proposal, you _should_ be getting stuck that way. That's how confused you've gotten me. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
