On Mon, Mar 2, 2015 at 9:02 PM, Jonathan S. Shapiro <[email protected]> wrote:
> 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?
I'd suggest either "nest" or "curried function type".
>> > 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,
You mean two applications, if I understand your cfn types. And since
real cfn 2-applications _are_ possible, we really can't be abusing
terms now.
> 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.
There are 3 result types in that type expression. You've wrapped the
second one in curly brackets. The way I'd express its significance is
that it's the result type of the outermost application that we're
looking at.
The two applications have been identified as a "group" that we can
easily optimize as a whole. The two corresponding cfns are not
separated by curly brackets.
> 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.
Oh. That takes care of some of my questions.
>> 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.
But you were saying things like that application needs to supply the
exact number of arguments to the left of some arrow in the type.
I say, contradictorily, that the application needs to supply the exact
number of arguments to the left of _the_ (outermost) cfn. There is no
choice in how many arguments a cfn application provides, given the
function type.
Maybe it's just you talking about curried applications instead of
individual applications again. I'm never going to understand you if
you keep doing that. It seems to me that when discussing function
types in detail, which is exactly what we're doing, you can't speak in
terms of an idiom (currying) which
1) Isn't a real part of the language (so far)
2) Is to be understood on top of the basic primitives that you're
still explaining.
>> > 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.
Oh I see. Arrow as in HM, concrete function type as in cfn. Sorry.
> 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.
Oh wait. No, I don't see. How can you specialize when the types are
already concrete? By "concrete" I mean closed, quantifier-free type
expression.
I just realized "concrete" means two things now with cfns being
"concrete" function types. Perhaps we should call them "native"
function types, or "nfns"?
>> > 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.
No, see, if I understand, you're saying unification of _curried_ cfns
requires that arities of corresponding cfns agree. But this is simply
a consequence of the rule for unifying individual cfns: They must have
the same arity, and corresponding argument and return types must
unify.
I am pleading that you not speak in terms of consequences for curried
whatever all the time. It's more complex than necessary, and it makes
it sound like you might've introduced some new type constructor where
we legitimately need to deal explicitly with the possibility of
currying.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
