On Mon, Mar 30, 2015 at 4:16 PM, Keean Schupke <[email protected]> wrote:
> On 30 March 2015 at 15:08, Jonathan S. Shapiro <[email protected]> wrote: > >> >> Oh. Oh dear. I think you have a bad assumption. Even if we are doing >> assembly-grain compilation, there are cases where we cannot know this. In >> particular, we may be a consumer of a function supplied by some other >> module/assembly whose type is 'a->'b->'c. In that case we don't know any >> restriction on the potential expansions of 'c. >> > > And we don't care about future expansions either. Consider "id". We can > pass a function to "id", and it returns the same function... > Actually, a similar thought had occurred to me, and I've been running around too hard to put it to words here. When we see "f a b c" and infer 'a->'b->'c=>'ret, we're making that inference because we have actually seen three parameters passed. A real return value is needed after those three parameters are passed, and this is true whether or not 'ret turns out to be of function type. So we actually don't care about the fact that 'ret might expand to a function type - it changes nothing about the return locus. That generalizes in the right way for all inferred arrow types. One of Matt's points in advocating AFN is that if the developer writes an *explicit* arrow type, The fact that it's an afn has the effect that the return position is *required*, and that no further specification of the 'ret type can remove that call/return position. In that view, we simply *can't* write the type a->b, but must instead write a=>b. Now if we adopt that view, then the whole concern about arrow types "expanding" on the right goes away. In fact, the need for => can be made to go away. The alternative is to simply say that given a type: a->b->c->'ret we should understand it as an afn type where the *last* arrow is interpreted as a =>, and the 'ret is understood to be wrapped in elided parenthesis. The parenthesis can be elided so long as 'ret is not an arrow type. So in this view, if 'ret turns into e->f, we'd rewrite as a->b->c->(e->f) and the parens are actually semantically significant. I'm not advocating any of this. I'm simply saying that we could abuse existing notation to mean what we need. If we try to unify a->b->c->'ret with a->b->'ret, we would get a->b->(c->'ret), which is consistent with what we've been saying before. It's equivalent to what I have previously written as a->b=>c=>'ret. The rule that the rightmost thing is understood as parenthesized also resolves what happens when programmers write these types explicitly. > I disagree, I don't care if a function returns a function, as long as I > have enough arguments to make the call. > You do care, because you can end up with **too many** arguments. Given f a b c f a b you really need to know that f can be called without a closure construction given only two arguments. You need to know this without yet knowing the concrete arity of f. > >> >> >>> >>> And arity concrete functions look like this (and may return further >>> functions): >>> >>> 'a 'b => 'c >>> >>> After concretisation all (curried) arity-abstract arrows disappear, and >>> are no longer valid in the type system, only (uncurried) concrete-arity >>> functions remain. >>> >> >> I think this is just a different notation for the cfns we have been >> talking about all along. I'd urge you to stick with the cfn notation in >> this discussion thread so that we don't have confusion about the meaning of >> the => arrow (which already has a bound meaning in the present thread of >> discussion). >> > > Which cfn notation? I don't like reusing the '->' arrow, as I want it to > be easily visible that all arity-abstract functions have been removed after > the concretisation pass. > > (cfn 'a 'b -> 'c) > > seems messy to me, if you don't like =>, how about: > > 'a 'b ~> 'c > I understand your distasted, but I respectfully insist that we stick with the "cfn a b -> c" form for this discussion. The tilde arrow is horribly easy to misread as a simple arrow, and we already have too many notations running around. I'm not suggesting that we want to keep the cfn notation in the final language. I'm saying that we should stick to a consistent notation in the present discussion in order to avoid the kinds of confusion that arose early in the thread. Feel free to parenthesize the cfn types explicitly if that helps you see them more clearly. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
