On Mon, Mar 2, 2015 at 10:37 AM, Jonathan S. Shapiro <[email protected]> wrote:
> Pun intended.
Nice.
> It's clear from my most recent exchange with Matt that we actually *don't*
> have a common understanding of how arity-concrete and arity-abstract
> application interact. I think we need to start over completely, go way back
> to basics, and work our way back up to something we can agree on. It's clear
> to me that the mechanism I have in mind works, and that others may as well.
> I think what we are hung up on is notation and the account for what that
> notation means. Let's start over. In fact, let's start by going all the way
> back to HM.
>
> Here are the statements that I think we can probably agree on:
>
> In HM, we have two facts:
>
> 1. The syntax
>
> f a b c
>
>
> is a convenience shorthand for
>
> ((f a) b) c
>
>
> and the syntax
>
> u->v->w->x
>
>
> is a convenience shorthand for
>
> u->(v->(w->x)
The ASTs are identical. I wish you wouldn't invoke the term
"shorthand" for that.
> 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.
Type theoretically, there's no such thing as a curried function. It is:
1) An informal idiom
2) Syntactic sugar to support the idiom
3) Some collection of implementation techniques to support the idiom
> 3. An application may have *fewer* actual parameters than the arrow type
> naively expects.
Nope.
> We often refer to this as a partial application, but that
> is a misnomer. Since all applications in HM take a single argument, there
> really is no such thing as a partial application. There are complete
> applications that return a value of function type.
Exactly.
> 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.
> provided (a) the total number of arguments consumed is not altered,
> and (b) combining is only performed at positions where an actual parameter
> is known to be present. What I mean by (b) is that given a partial
> application
>
> (f a) b
So this is a couple of cfn applications, and multi-arg cfn
applications are allowed, so we need the parens. Got it.
> 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.
> That's the part that will get returned as a function
> object that may (or may not) get applies elsewhere. Based on what we can see
> in front of us at the application site, we don't know enough to optimize the
> arity of that return value.
>
> However, based on what we know at the application site, we *do* know that
> two arguments are present to consume, and this justifies us in co-rewriting
> the application and its type as
>
> (f a b)
> cfn u v -> { cfn w -> x }
>
> respectively.
This makes sense.
> So far so good. This much, I think, we probably all agree on.
Basically, yes.
> I suspect we can also agree on the following two statements:
>
> 6. The additional restriction in BitC is that we disallow partial
> applications (in the absence of explicit syntax). The consequence is that
> the number of arguments consumed by the application (that is: up to, but not
> including, the part of the type in the brackets) must exactly match the
> number of actual parameters that are present.
On Mon, Mar 2, 2015 at 10:50 AM, Jonathan S. Shapiro <[email protected]> wrote:
> CORRECTION!
>
> We disallow partial applications of concrete functions. My intention is that
> given the function type
>
> f :: cfn u v -> (cfn w -> x)
>
>
> the application
>
> f a b
>
>
> is perfectly valid, and returns a value of function type.
>
> Informally: there must be *some* arrow present in the concrete type such
> that the collective stuff to the left of that arrow exactly consumes the
> number of actual parameters present.
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?
For example, this is wrong:
f :: cfn u v -> (cfn w -> x)
f a b c
This is OK:
f :: cfn u v -> (cfn w -> x)
(f a b) c
If we wanted to change it to a single application:
f :: cfn u v w -> x
f a b c
> 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?
> 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.
Also, what are the rules for curly brackets?
And to confirm: Unification of cfns does not in any way involve the
rewrites you were just talking about.
> I have attempted to introduce an arity type variable to address this
> requirement, and I have apparently created a fair bit of confusion. What I
> think we *can* say about this is that *some* sort of unifiable thing
> (presumably a variable) must exist to capture the notion that there can only
> be a single concretization of a given type in a given specialization.
Yes, like for the choose_one example. I think I probably know what you
meant with the requirement at the beginning of (7) now. "the" was the
instance of the abstract type for any given closing substitution of
the quantified variables.
> 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? My understanding was that the point of arity abstraction
was that we would _not_ think of arity adjustment as rewrites, but as
specialization. We go from abstract to concrete, not from one concrete
type to another.
> The next step will be to figure out how to "lift" all of this
> into the type system so that we can talk coherently about what happens when
> arity is part of semantics. The two rules BitC introduces are:
>
> B1) No hidden allocations
> B2) No arguments based on "optimizer makes right"
>
> My sense is that we are all in agreement about what can practically be done
> in the presence of those two rules. What we seem to be struggling with is
> how to express the specialization rule.
Agree.
> Before I go on, I want to confirm that we are actually in agreement about
> the points above. PLEASE (just for now) restrict responses ONLY to the
> points I have made above. A wandering discussion is very disruptive. By all
> means ask other questions, or fork the thread to pursue side questions.
My unrelated responses are all on the old thread.
> When
> you do so, CHANGE THE SUBJECT LINE. If I have missed an important thing that
> we know, please bring it forward. We'll get to the lifting discussion in the
> next step, but let us try to start from common ground when we do.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
