I'm not sure if this has been answered yet... On Mon, Feb 23, 2015 at 12:57 PM, Matt Oliveri <[email protected]> wrote:
> On Mon, Feb 23, 2015 at 12:26 PM, Jonathan S. Shapiro <[email protected]> > wrote: > > > I'm thinking this is probably clarified by now, but just in case.... > > > > 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. > Except there are more, because when > we plug in any nat except 4, a new variable pops up out of nowhere. Normally, fresh variables are implicit in the source, but they are not > implicitly added by plugging in concrete elements for other variables, > I thought. Ah. I see the issue, and you are correct that this is an unusual specialization in that regard. Here's the intuition: A curried function having type a->b->c->d->r can be partially applied, with the result that a closure is obtained. The closure in turn has a function type reflecting any residual arguments that were not determined at the time of application. If the initial function type is abstract, and we only make the arity concrete for the leading arguments, any remaining arguments remain just as abstract as they were before. 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. In effect, we have done a partial specialization, analogous to what happens when Ctor 'a 'b is unitifed with Ctor int 'u - the result of the specialization is not yet wholly concrete. I agree that the choice of syntax for the type isn't making this easy to understand at first glance. Note that the only way the return type of T2 can be abstract is if 'v or 'w is abstract. 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. > Your notation seems to be bending the rules and you haven't > acknowledged it. In summary, I don't understand because the notation > for arity-abstract types suggests a formal system in which abstract > types don't have all the concrete instances they should. > An arity-abstract type can indeed have any of the concrete instances you suggest. In a fully specialized program (a precondition for execution), an arity-abstract type will end up having exactly one concrete instance for any given specialization. This is the same as the rules for any other specialization. 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. When unification occurs between a type having N type variables and a second type having M type variables, the unification result may potentially have N+M type variables. Or, in the case where one of the types being unified is [partially] concrete, it may have fewer. That's what is happening here. > > The arity variable is a type variable having Nat kind, which means that > is > > has to specialize to a natural number. > > I figured that. That's why I referred to arity-abstract types as > arity-indexed type families for a while. Then I realized that wouldn't > work if arities are nats representing the "shallow" arity of the first > application. > > One of the solutions is essentially Keean's notation for "deep" arity. > You can represent it with type-level lists of nat. Legal deep arities > for the example type: > [4] > [3,1] > [2,2] > [2,1,1] > [1,3] > [1,2,1] > [1,1,2] > [1,1,1,1] > So 8 concrete instances. > Yes. I didn't do that because I find that notation of arity confusing. I'll probably get used to it. But the other reason is: it doesn't matter. Since the unification/specialization process proceeds left to right, we are never interested in more than the shallow arity of the first application in any given unification. > Before I forget, another question I have about the notation is how to > read off the maximum arity when the return type is a variable. You can't, because the maximum arity (which I take to mean the sum of the list elements in your lists] is underspecified until the return type is concretized. It can become sufficiently specified sooner, but there is no guarantee that it will. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
