On Mon, Mar 2, 2015 at 1:45 PM, Matt Oliveri <[email protected]> wrote:
> On Mon, Mar 2, 2015 at 9:11 AM, Jonathan S. Shapiro <[email protected]> > wrote: > > > 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)))) > > It sure is, courtesy of the parser. But you have to admit, adding back > the "fn" prevents the "shorthand" from being literally the same parse > tree as the longhand. > When I was asked at the beginning of this discussion what 'fn' meant, I said that it was purely a form of syntactic bracketing to allow us to write multiple arguments to the left of the arrow without introducing parse ambiguities. Once we start introducing an arity marker, that is no longer true. I wrote it in my question above mainly out of force of habit. Also because I was anticipating re-introducing the arity later in the discussion and I didn't want to switch surface syntax abruptly. Switching is confusing too. > In other words, if anything, > fn 'a->'b->'c->'d->'e->'r > parses as > fn 'a->('b->('c->('d->('e->'r)))) > but I thought we are not accepting ('e->'r) as a well-formed function > type under your proposal. So it doesn't actually parse that way. > There's only one function type here. > I agree there is only one function type here. The parse you give above is what I intended. > So adding back the "fn" is not entirely trivial. If you wanted > fn 'a->'b->'c->'d->'e->'r > to be shorthand for > fn 'a->(fn 'b->(fn 'c->(fn 'd->(fn 'e->'r)))) > which, without arity abstraction, you would, then you have to > "ungroup" the function type... In the absence of an arity marker it's just a syntax manipulation. > 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? > > Why give such a complex explanation of "'a->'b->'c->'d->'e->'r"? Because I am leading up to a discussion of how specialization works in order to account for how arity specializaiton works. > >> > that is: the conventional arity notation is a convenience shorthand > for > >> > the > >> > fully nested one. > >> > >> 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? > > Yes. But that kind of thing is below the radar for this discussion. > Well, no, apparently it isn't. The confusion in the present discussion drives us all the way back to basics to sort things out. > The parser sees them as nested. They are nested. The type system > doesn't need to address curried functions, as I explained above. > Matt: that's your *assumption*. But in the presence of arities (which I was about to re-introduce), it is not at all clear that what you say is still the right interpretation. > >> > 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). > > But that _does_ prevent partial applications, in this case! If 'r gets > instantiated before 'arity, we might forget the upper bound if we > hadn't made it explicit. At least that's the case if you allow > ungrouping. > Misplaced referent. If you are referring to the arity notation, that does NOT prevent partial applications, because it says that the application may consume 1, 2, 3, or 4 arguments. There is no assurance of arity agreement inherent in this notation. > > But we *do* need a variable present to reflect the fact that the concrete > > specialization involves a particular sequence of concrete arities. > > And also to let us impose upper bounds, maybe. > Perhaps. But that now seems uncertain to me, and I was intentionally trying to state the least requirement that motivates the variable. > > >> > 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. > > But > ('nargs >= 4) => fn 'nargs 'a->'b->'c-'d->'r > could concretize to > fn 4 int->int->int->int->bool > for example, and that's an incompatible concrete arity with > fn 1 int -> fn 1 int -> fn 1 int -> fn 1 int -> bool > assuming they are, in fact arity-concrete. > If we are talking about the nArgs approach, then the mental model is that we are starting from the curried version and then using further rewrites to work our way up to the fn 4 version starting from the fn 1 -> fn 1 ... version. The idea in this notation is to follow the optimizer rewriting model. Yes, the two concrete arities you give are incompatible, in the sense that they do not unify. > So you cannot say > ('nargs >= 4) => fn 'nargs 'a->'b->'c-'d->'r > is shorthand for > fn 1 'a -> fn 1 'b -> fn 1 'c -> fn 1 'd -> 'r > because then they'd have to be equivalent types, but only the former > has the concrete-arity-4 instance. > No, Matt. I switched notation here intentionally in order to use a completely different approach. I'm saying that: ('nargs >= 4) => fn 'nargs 'a->'b->'c-'d->'r is [definitionally] shorthand for fn 1 'a -> fn 1 'b -> fn 1 'c -> fn 1 'd -> 'r and that what we are then going to do is combine arities as we further specialize the CONCRETE function type in order to do optimizer-style combinings to arrive at higher arity. > > 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. > > Viewing that syntax as an arity-concrete function type seems at odds > with viewing "fn 'arity 'a->'b->'c->'d->'r" as shorthand. You _need_ > to keep the argument types grouped, because you don't _know_ if it's > curried or not. > The "2" tells me the concrete arity, so how is it that I don't know what it is? > > 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. > > No, my latest thinking is that they should always be nestable. > > We need to address whether they can be ungrouped freely, like you seem > to be doing with > ('nargs >= 4) => fn 'nargs 'a->'b->'c-'d->'r > as shorthand for > fn 1 'a -> fn 1 'b -> fn 1 'c -> fn 1 'd -> 'r > > To me, that's nonsense, and the nonsense is especially clear in this > case, since only the latter function type has concrete arity. In fact, > it was because this seems so obviously nonsensical to me that I > assumed that "fn 1 'a -> ..." was not intended to be arity-concrete, > so I introduced "cfn" and "afn" to disambiguate. But it seems that's > not what you meant. > Indeed. My intention with the 'nargs notation was to move immediately to concrete arity based on currying, and then explore optimizer-style rewrites. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
