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? > > 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? > 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. > > 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. One step at a time. Forging ahead too quickly is part of how we have been getting in trouble in this conversation generally. This thread is intended to be a "from nothing", completely de novo re-start of the conversation. Nothing from the previous threads is relevant in this one. > 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. > >> > 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. > 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. > >> > 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". 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? 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. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
