On Tue, Mar 3, 2015 at 10:46 AM, Jonathan S. Shapiro <[email protected]> wrote: > On Mon, Mar 2, 2015 at 8:35 PM, Matt Oliveri <[email protected]> wrote: >> >> On Mon, Mar 2, 2015 at 9:02 PM, Jonathan S. Shapiro <[email protected]> >> wrote: >> >> >> 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. > > This confusion is parallel to the one we had about arrow types. The > application that you are referring to is the single-step application. The > application that I was referring to is the result of the expression: > > f a b > > which we colloquially refer to as "an application". What terms should we use > to differentiate these two things in the present conversation?
I like referring to the single-step application as "application" since that's the actual language feature. I use "n-application" for an application with arity n. Multiple nested applications can be called a "curried application", analogous to "curried function type". The syntax I've been using for possibly-multi-arg applications is: (f a) b // Two 1-applications (a curried application) f a b // One 2-application (only degenerately curried) >From your last email, I thought you were using this syntax on this thread for cfn applications, but just now I think you used (f a b) for two 1-applications. For cfn applications, we might want to use alternative syntax, to make it really easy to distinguish from other types of application where native arity may not need to exactly match. We could also shorten "cfn application" to "call", if you like. We'd need to be consistent about calling non-cfn applications something else. Here is C syntax for calls: f(a)(b) // Two 1-applications (a curried application) f(a,b) // One 2-application (only degenerately curried) >> > 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. > > Same referential ambiguity as above. You are focusing on the result type of > the step-wiae applications. I was referring to the result type of the > expression. Once again, how can we keep these things unambiguous in the > current conversation? So in (a->b->c), there are two function types, but three curried function types: a->b->c // One step, returns (b->c) b->c // One step a->b->c // Two steps, returns c We can systematically disambiguate ambiguities like the one between the first and last with deep arities: a->b->c // One step, arity [1] a->b->c // Two steps, arity [1,1] (List notation is silly when all functions have arity 1, but deep arities for curried cfns need to be lists.) So clearly there will be a lot of curried function types we don't want to talk about. One that we want to point out can be designated as a "group". So roughly, "group" is an alias of "curried _", but with the intent of being used only for certain curried whatevers that we care about. Equipped with "group", we could also say the curly bracket part was the return type of the group. >> 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. > > That is true, and that is as I intended. The curly brackets are present to > indicate which part of the type constitutes the expression result. Without > knowing that, we won't be able to deal with partial application restrictions > later in the discussion. Agree. (That's actually why I thought you were adding it to the type system. But I'm glad you didn't.) >> > 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. > > Matt, I'm just in the first step of introducing this discussion. Please > don't restrict *my* notation quite yet. Ultimately, the whole problem here > is that we are going to need to deal with the arity issue. At *that* point > we will talk about AST rewrites and multiple arguments. OK, so you meant what you said. I thought you were implicitly talking about curried applications again. Never mind. I need to go back and clarify. >> 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. > > I don't see how we can *avoid* doing so, because we are not merely > discussing types. We are discussing the transformation from curried to > arity-aware types and the consequent re-writing of ASTs. We need to discuss > all of these things in lock-step to arrive at a coherent final outcome in > the discussion. Because of the [forthcoming] arity issue, curried syntax in > BitC is not merely an idiom. I agree, but for just cfns so far, I thought currying could still be treated as an idiom. By not speaking in terms of the currying idiom, I mean you should not just say "application" when you mean "curried application", and analogously for other curried constructs. You can still talk about currying without causing confusion as long as it's clear you're talking about currying. That's all. >> >> > 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. > > Yes. > >> > 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. > > We're going to get to that, and I'm not sure "specialize" is the right term. > But what I was referring to above was specializing the arrow type. Alright. >> I just realized "concrete" means two things now with cfns being >> "concrete" function types. Perhaps we should call them "native" >> function types, or "nfns"? > > No, they do not mean too different things. I'm suspicious, but I'll let you go on. >> >> > 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. > > I'm not sure what you mean by "curried cfns". Like this type: cfn a b -> cfn c d -> r // Arity [2,2] If we want it to be equal to: cfn e f -> cfn g h -> q then we want: a = e b = f (cfn c d -> r) = (cfn g h -> q) There was only one arity to compare. >> 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. > > How do you propose that we talk about an application syntax of the form > > f a b > > without referring to currying? Well, I thought that's a 2-application. > The whole point of the current discussion is to arrive at a consistent > method for re-writing the curried application surface syntax into the > corresponding fully disambiguated, parenthesized, and arity-aware > application syntax. Yes. I clarified how I think we can talk non-confusingly about currying in a later (than the one you replied to) email on this thread. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
