On Sun, Mar 1, 2015 at 9:58 AM, Matt Oliveri <[email protected]> wrote:
> On Sun, Mar 1, 2015 at 11:35 AM, Jonathan S. Shapiro <[email protected]> > wrote: > > On Sat, Feb 28, 2015 at 8:19 PM, Matt Oliveri <[email protected]> wrote: > >> > >> Let me know if you can nest arity-abstract function types. Like: > >> fn 'ar1 'a->'b->'c->(fn 'ar2 'd->'e->'f) > > > > I am not sure how to answer this, because in one sense the answer is > "yes" > > and in another sense the answer is "no". > > Uh oh. That was supposed to be a pretty concrete question. It's > amazing, in a bad way, how two people can look at the same incomplete > explanation and invent entirely different details to fill the gaps. > > > Let's ignore arity for just a moment in order to ask this question more > > generally: if we are working with HM-style function types, can you nest > > *those* in the way that you ask? That is: is there any difference between > > > > fn 'a->'b->'c->'d->'e->'r > > > > and > > > > fn 'a->'b->'c->(fn 'd->'e->'r) > > > > I think the answer to this is obviously "no". Or alternatively, the > answer > > to this is obviously "yes", and we should understand > > > > fn 'a->'b->'c->'d->'e->'r > > > > as a shorthand for: > > > > fn 'a->(fn 'b->(fn 'c->(fn 'd->(fn 'e->'r)))) > > I think the answer is that "fn 'a->'b->'c->'d->'e->'r" is a syntax > error. HM function types always take one argument. > And yet we very commonly see HM function types written as 'a->'b->'c->'d->'e->'r So ignore the 'fn' in what I wrote above, go back, and please answer my question. We cannot make progress without that starting point. Re-writing in something more recognizably HM, given the two types: 'a->'b->'c->'d->'e->'r 'a->'b->'c->('d->'e->'r) That is: that the parens here are solely for purposes of precedence breaking, and in this case they have no effect on the type and the two types are therefore identical? [Expected answer: they are the same.] Do we also agree that in a curried language, *all* arities are 1, and therefore we should understand the type 'a->'b->'c->'d->'e->'r as a shorthand for: 'a->('b->('c->('d->('e->'r)))) That is: arguments are consumed one at a time until we run out of arguments, and any remaining portion of the function type survives as the return type of the returned value? > > > that is: the conventional arity notation is a convenience shorthand for > the > > fully nested one. The only sense I can see in which this is *not* a good > > interpretation is that we don't know whether 'r will end up unifying > with a > > function type, and our nesting may get deeper as a result. That seems a > > little odd for a convenience shorthand, but certainly not impossible. > Merely > > odd. > > What is the "conventional arity notation"? > Is that "fn 'a->'b->'c->'d->'e->'r"? > Or "fn 'arity 'a->'b->'c->'d->'e->'r"? > Or something else? > I'm very sorry. The word "arity" in that sentence should have read "arrow". So: The conventional _arrow_ notation is a convenience shorthand for the fully nested one. Does that make the proposition clearer? You might not follow the above because AFAIK you consider (fn 2 > 'a->'b->'c) to be literally, syntactically the same as (fn 'arity > 'a->'b->'c), once you've substituted ('arity := 2) Well, no. Obviously I do not, because I keep saying that this substitution (at least in the general case) requires us to introduce a new arity variable, because 'c could still unify with a function type! > How about, for the time being, we use (cfn 2 'a->'b->'c) and (afn > 'arity 'a->'b->'c)? Definitely not. If we are forced to that, then the arity discussion is over and BitC will not support currying at all. Let's work first to see if we can come to agreement about nesting, given my clarifications. Hmm. Maybe that's too strong. My intuition is that arrows need to be a single type, and that multiple arrow types are a bad idea. Take this in steps, Matt. The essential issue here is that you are struggling with the substitution rule that I have proposed, and I haven't answered your questions about it adequately yet. Don't jump the gun quite yet. > So another way to look at this would be to write > > it as: > > > > f :: ('nargs >= 4) => fn 'nargs 'a->'b->'c-'d->'r > > Now you're getting weird. From your previous email, I thought the > point of ('arity < 5) is to prevent partial applications. Not at all! The ('arity < 5) notation means simply that there are 4 arguments present, and therefore (a) the *first* concrete application may not consume more than 4 arguments nor less than 1, and (b) it's return type must be something that might account for the *rest* of the arguments (if any remain). The ('nargs >=4) argument is coming from the opposite perspective, but on reflection I don't think that it works. What it was trying to capture is "since 4 arguments are present, f must be a composition of functions that will, when applied in sequence, consume 4 arguments without introduction of a hidden allocation". It could consume more because the return value of the function might be a function type. > I don't > understand how ('nargs >= 4) prevents this. We don't need to say > anything additional to see that f can be applied to at least 4 > arguments, because its arity-abstract type already lists 4 argument > types. We can safely apply more arguments than the native shallow > arity might turn out to be. > But we *do* need a variable present to reflect the fact that the concrete specialization involves a particular sequence of concrete arities. I agree with you that an *abstract* arity variable (in either form) does not add new information w.r.t. the number of arguments required. It exists only for the purpose of ensuring that when two abstract-arity function types are unified, they unify in such a way that they end up with the same concretization at all points. > > with the intended interpretation that f is some [composition of] > functions > > such that f takes at least four arguments, and may take more depending on > > how r unifies. Following the arity-free convenience syntax intuition > above, > > this can be viewed as a shorthand for: > > > > f :: fn 1 'a -> fn 1 'b -> fn 1 'c -> fn 1 'd -> 'r > > Whoa, I didn't know that. I thought that type was arity-concrete (up > until you get an 'r, which may be an arity-abstract function). > It is. What I'm writing here is how this would expand to a curry-style application, where all arities are concrete and all arities are 1. > > where 'r is completely free, an in particular may unify with fn 'nargs > ... > > for any 'nargs, but simultaneously need not unify with a function type at > > all. And in *that* interpretation of things, we're saying that we are > > permitted [inductively] to combine smaller arities into higher arities > and > > rewrite the application AST, such that (inductively) > > > > fn 1 'a -> (fn 1 'b -> 'c) > > > > may be "composed" into > > > > fn 2 'a->'b->'c > > So how would you actually write a function type whose native shallow > arity is 2? I'm starting to think I actually have a quite-different > proposal from yours, and that we should start over, explaining our > proposals in more detail. > We have used several different notations. In our current notation, I would write an arity-concrete function having arity 2 as: fn 2 'a->'b->'c which is what I wrote above. > which may in turn be combined further. So in this view we are starting > with > > all arities equal to 1 (which is the curried view) and coercing the > arities > > *upwards* within the type rule for /app/. > > > > This actually might be a more consistent and simpler way to think about > > things. > > But what drives specialization? How do you talk about the types of > defined functions, which are arity-concrete, and how they unify with > arity-abstract function types? > Application drives it. > > I'm not sure whether this is helping or not, so I want to stop here to > give > > you a chance to read and see if you can help refine either the question > or > > my answer. > > It's helping by uncovering massive differences in our thinking. > Well, I suppose that's progress. > > Haven't forgotten the other question, but I think that refining this one > may > > possibly lead us to a different answer there, so let's tackle this one > > first. > > It seems you want afns to be nestable. But, unlike me, you think afns > can be "groupped" or "ungrouped" between nested afns. And you don't > seem to have cfns in your syntax at all. Yes, we probably should work > this out before (or at the same time as) we worry about how the arity > parameter of an afn is interpreted. > It seems to me that we haven't come to a common understanding of whether fns of any sort are nestable, and that's where we need to start. I think the afn/cfn distinction is very, very problematic. For me, the grouping of nested afns, assuming it's allowed, reflects > the individual arity-abstract applications. We cannot regroup them > because that would change the requirements on the concrete instances. > Each arity-abstract application, individually, must not specialize to > involve an arity-concrete partial application. In other words, it must > specialize to one or more exactly-matching arity-concrete > applications. I'm with you up to this point, but then you write: > You cannot split an arity-concrete application between > two arity-abstract applications. > But Matt, there *are* no arity-abstract applications. The only *real* applications are the arity-concrete applications! shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
