On Mon, Mar 2, 2015 at 4:46 PM, Matt Oliveri <[email protected]> wrote:
> > 2. An application must consume all actual parameters. This is ensured by
> > checking the arrow type. The arrow type must have **at least** as many
> > positions to the left of the arrow[s] as there are actual parameters. It
> may
> > have more, it may not have less.
>
> This is a misleading way to say it. The arrow type has one argument
> position. It's return type may be an arrow with its own argument
> position. Etc. An application must consume exactly one argument. The
> result may be applied to exactly one argument. Etc.
>
Thank you. You're completely correct. Just to clarify, here and a bit later
when I wrote "the arrow type" I was referring to the extended surface
notation, as in
a->b->c->d->r
I'm not sure what we should call that, but hopefully my comments make more
sense if read with that explanation in mind.
What *should* we call that?
> > 3. An application may have *fewer* actual parameters than the arrow type
> > naively expects.
>
> Nope.
>
Again, I meant in the extended (multi-arrow) arrow type.
> > 4. Optimization of procedure application in HM is non-semantic, but it
> has
> > to preserve the rules that I have stated above. All arguments present
> must
> > be consumed. By the time of optimization, all type variables are fully
> > concretized, and when that is true we can justify rewriting the HM-style
> > arrow notation using the arity-concrete notation:
> >
> > cfn u -> (cfn v -> (cfn w -> x)
> >
> > having done so, the optimizer is free to "combine" arities into larger
> > arities,
>
> I don't see the significance of switching to "cfn" notation if we're
> still allowed to mess with the concrete arity... Oh I see, you can
> also have multi-arg cfns.
>
That, and I'm trying to emphasize for the moment that I'm talking about
concrete (implementation level) function types rather than potentially
"higher level" arrow types.
> > we have to look at our concrete type as:
> >
> > cfn u -> (cfn v -> { cfn w -> x })
> >
> >
> > where the curly brackets indicate the "unapplied" portion of the type.
> That
> > part cannot be re-combined by the optimizer, or at least not without a
> lot
> > more information.
>
> So the curly brackets seem to be indicating a group boundary, and we
> can't (easily) mess with arity across group boundaries, because then
> the corresponding application rewrites might be all over the place.
>
I'm not sure what you mean by a "group boundary". All I was trying to
indicate here is that if you are applying that type in an application that
presents two arguments, the stuff in the curly braces is necessarily the
*result* type, and the stuff to the left of the curly braces is the part
that consumes the arguments at the application site.
I didn't intend to be changing the type here. I was merely trying to
indicate where the boundary was between the applied part and the result
part.
> I thought the purpose of your cfn notation was to to change the
> concrete type and application simultaneously. At any given point, the
> concrete application arities exactly match the applied cfn arities.
> This is actually the same as in the HM optimizer case. So what
> changed?
>
Since I have never used the cfn notation before this message, I'm not sure
why you think that. I'm intentionally changing notation to break
associations with the previous discussion.
But yes, the AST probably needs to be rewritten in the way that you say. I
simply wasn't focusing on that aspect of the discussion here.
> 7. Where two arrow types unify, the corresponding concrete function type
> > must unify. This is necessary to ensure (e.g.) assignment compatibility.
>
> I don't understand this statement. My understanding of abstract types
> is in terms of quantifiers. What is "the" concrete function type
> corresponding to an abstract function type?
>
I haven't introduced any quantifiers in the present discussion, and that is
intentional. The quantifiers are what is getting us in trouble.
What I'm saying here is simply if you specialized one "copy" of an
[identical] type, you need to specialized all the other's the same way. You
can specify different *instances* of a type separately, but the same
instance of a type only specializes one way in a given specialization.
> Unification of cfn types requires that arities at corresponding positions
> > must agree.
>
> You don't need to say "at corresponding positions". Each cfn has one
> arity. Thinking of nested cfns as one thing having multiple arities is
> really going to confuse me for this discussion.
>
Then get used to being confused, because I suspect we are going to need to
talk about this.
> Also, what are the rules for curly brackets?
>
They are only a visual indicator of what constitutes the return type.
> And to confirm: Unification of cfns does not in any way involve the
> rewrites you were just talking about.
>
That's kind of the next part of the discussion.
> > Up to this point in the discussion, I think that we are all fairly well
> in
> > agreement.
>
> I'm afraid I'm not yet on the same page as you. Aside from answering
> questions above, what is the relation between arity rewrites and
> unification?
I intentionally have not yet spoken about that yet. That's the next part of
the discussion.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
