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: > 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.
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. However, you seem to say later that it unifies with more than four concrete types, and I say that semantically, it should have more than four concrete instances. So the way you're doing unification, and the variables you're using don't seem to match. >> 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. Yes. > 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. > 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. The big difference is that there's no problem explaining that unification in terms of quantifier manipulation. Starting with (Ctor 'a 'b), weaken with 'u, then intantiate 'a to int and 'b to 'u. With T1, weaken with 'newArity, instantiate 'arity to 2, magic happens, and now 'newArity is being used by a function type that didn't used to be there. > 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. > 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. >> 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. Yes. > 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? > 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. New variables can appear by weakening. That's not what's bothering me. >> > 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. 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. 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? In particular, how do we know that choose_one's type fn 3 (fn 'ar a->b->c->d) (fn 'ar a->b->c->d) Bool -> (fn 'ar a->b->c->d) doesn't unify with fn 3 (fn 1 a->fn 'a1 b->c->d) (fn 1 a->fn 'a2 b->c->d) Bool -> (fn 1 a->fn 'a3 b->c->d) aside from that it makes no semantic sense? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
