On Sat, Feb 21, 2015 at 6:56 AM, Keean Schupke <[email protected]> wrote:
> On 21 February 2015 at 11:18, Matt Oliveri <[email protected]> wrote:
>> You just pretty much described dual (application-driven) arity
>> specialization. Well done. But I thought it was you who said we'd
>> handle the HOF case by specializing the HOF, if it's in the same
>> module. The function whose arity we are thinking about is not the HOF,
>> it's what the HOF calls. So specializing the HOF would be
>> definition-driven, not application-driven. We are specializing the
>> code for how the HOF calls its argument to suit the actual argument's
>> definition.
>
> I think that we can consider the specialisation just a form of inlining.
> Consider:
>
> f :: Nat -> Nat -> Nat
> f = ...
>
> f 1 2
>
> Applying f to 1, returns a function that we apply to 2 to get the result.
> Although this is safe (we don't allocate for lambda-accumulators) it still
> involves two function calls. You could inline the first if you have access
> to the definition. But I think now this makes no difference to
> type-checking, its an implementation detail.
OK, so I have no idea how that constitutes a response to what I said,
but anyway...
You seem to be contradicting your earlier story. Before you said that
an expression like (f 1 2) applies two arguments at once, so it wants
f to have an arity-2 type. But now you're saying it's two function
calls before optimization. That _would_ be safe, but it's not what
your proposal does.
With (f 1 2) being a 2-application, if we didn't inline, we would need
to coerce f to an arity-2 type, which would allocate. In this
approach, the inlining is not an optimization, it's a requirement to
avoid allocation.
More generally, the fact that you liken your specialization proposal
to inlining makes me even more doubtful that the cases where subtyping
isn't allowed can be captured simply.
> The only change I was suggesting, is based on the fact we can do this
> inlining, we may as well infer the most-curried type for all functions, as
> we know the inlining will remove the applications later.
You don't know inlining will fix anything in general, unless you have
the whole program, and even then, it probably isn't practical to do so
much inlining.
>> Well, as long as we agree that the final program doesn't have any
>> isolated coercions from one function arity to another. I see these
>> coercions as the implementation of the subsubption rule, so no
>> coercions means no subsumption. Of course I see that the way you do
>> type checking in the first place would use the subsumption rule. Then
>> subtyping triggers specialization by rewriting the derivation to not
>> use subsumption anymore, essentially. That's how I understood your
>> proposal. And my problem is that this idea is brand-new to me, and
>> there seems to be a lot of flexibility (ambiguity) in the details,
>> which you haven't been explaining very systematically.
>
> consider 'g' to be an implicit parameter,
Why? It's fine as a static dependency.
> consider:
>
> import g :: Nat -> Nat -> Nat
> main = g 1 2
>
> main :: {g :: fn Nat Nat -> 'a} -> 'a -- if we type main in isolation
> treating 'g' as an implicit parameter we don't know its return type.
>
> Now we can pass 'g' in implicitly using normal subsumtion. So we don't need
> anything other than the subtyping relation. No type coercions at all (just
> the inlining optimisation to improve things).
There is a coercion! From (Nat->Nat->Nat) to (fn Nat Nat -> Nat). I am
assuming (Nat->Nat->Nat) is short for (fn Nat -> fn Nat -> Nat), since
your proposal doesn't use arity-abstract types. Inlining would remove
that coercion, which is why it's not just an optimization in your
proposal.
>> No, I don't think you do. You know what functions need to be
>> specialized from the combination of
>> 1. Their type
>> 2. The type of actual arguments they get applied to
>>
>> That's not quite as simple.
>
> Hmm, this is just type inference.
I suppose that is simple enough, considering that you're not doing
this at link time. The big problem is the mandatory optimization.
>> >> It's clear from what you said now that your proposal is truly
>> >> different from Shap's. So that answers your question. Now my question
>> >> is: What do you think are its advantages and disadvantages. This will
>> >> give people perspective about your decisions. (Or allow them to reject
>> >> it out of hand.)
>> >
>> > Advantages are greater efficiency (less function applications).
>>
>> So I would attribute that to the combination of definition-driven and
>> application-driven specialization. Is there more to it than that?
>
> Perhaps there is no difference apart from the type-system? Perhaps I am just
> trying to understand this from my personal experience. If you remove the
> inlining of applications and inferring the most-curried type for the
> definition, its now looks the same to me.
You cannot remove the inlining. That would allocate. The more you
talk, the less similar to Shap's proposal yours seems. (I see you
chose not to answer my question.)
>> >> As far as the example, I did not break the code there across modules
>> >> since that's not what confuses me about Shap's proposal. But with your
>> >> proposal, the examples you should give are the various cases of
>> >> specialization which apparently hinge on where the functions come
>> >> from.
>> >
>> > Its simple, you specialise the definition where you can (you have access
>> > to
>> > the source), otherwise you cannot and you have to use the definition you
>> > actually have imported (say from 'C').
>>
>> That's still ambiguous, I think. We need to be absolutely positive
>> that we reject all cases where specialization won't eliminate all
>> instances of subsumption. The difficult task you have burdened
>> yourself with is convincing Shap that you know all those cases.
>
> Considering free variables as implicit arguments, allows the use of normal
> subtyping subsumption, so we can be sure that all applications are sound.
No. That's the theme of this email: No, because those subsumptions are
coercions that allocate. They need to be eliminated somehow. You have
to prove they will be eliminated.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
