On Tue, Mar 3, 2015 at 3:16 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Tue, Mar 3, 2015 at 11:45 AM, Matt Oliveri <[email protected]> wrote: >> >> On Tue, Mar 3, 2015 at 10:46 AM, Jonathan S. Shapiro <[email protected]> >> wrote: >> > > >> > 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. > > I'm fine with "n-application" meaning "a [potentially progressive] > application of a function to n arguments". But that's not the same as an > application having arity n.
No deal. I don't want "n-application" to possibly involve multiple applications. It's just an application. It seems fine to me, since there's only one thing the n could be. If that term is not acceptable, I'd still like something shorter than "application having arity n". > Arity is a property of the function being > applied, not a property of a [potentially progressive] application. Well there are multiple notions of arity, and I don't see why we can't talk about the arity of applications. >> Multiple nested applications can be called a >> "curried application", analogous to "curried function type". > > Please write out what a curried application looks like, in your mind. My > example "f a b" intentionally took now position on whether f had arity 2 or > f had arity 1 and returned something that had arity 1. > > And I'm completely unclear here how a curried function type differs from an > arrow function type. I think I answered these further down in the last email. >> 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. > > Neither. Throughout, I have explicitly taken no position on how many > one-step applications are involved in (f a b). Well, when you wrote your example cfn rewrite back at the start of this thread, you happened to correctly use my syntax above. I guess that was just informal. > It's clear in hindsight that > we need to be syntactically explicit in these notes, and that we should > probably use different brackets to do so. I'm in the middle of something at > the moment. I'll bring forward an annotation for this in my next note. I agree. I'm looking forward to an exact-arity-matching syntax we can agree to use. >> 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)/. > > Yes, but I REALLY don't want to use C-syntax in the present discussion. It > conflicts horribly with other uses of parentheses. I'll take your word for it. In SML, it works out that if you always use C syntax for function calls, it parses right, like 95% of the time. 'Course in SML it's a tuplized application. Mixing C-looking and curried-looking syntax doesn't work so well without extra parens. >> (List notation is silly when all functions have arity 1, but deep >> arities for curried cfns need to be lists.) > > I'm coming to agree about the need for list arities. :O > I have no idea why we > are talking about curried applications of cfns. What in tarnation does that > mean? You seem to mean something different by "curried" than me. > By the time a cfn is introduced, any ambiguity about number of > consumed arguments should be explicitly resolved. Sure. And if you chain them, to idiomatically take more arguments, it's currying. >> >> >> > 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] > > You know, I'm starting to feel terribly confused about what the hell is > meant by "curried". It seems to me that the whole concept of currying only > arises when (a) applications may be done in boxcar fashion, and (b) the > number of arguments consumed at each step is intentionally left uncertain. > Neither of these statements is true in your cfn type above. I agree with (a), but I don't see why that can't be done with cfns. Maybe I don't know what you mean by "boxcar fashion". (b) seems particular to arity abstraction, which we haven't even gotten to yet. If you demand (b), then HM doesn't have currying because the number of arguments consumed at each step is 1. Maybe I don't know what you mean by "step". The way lambda calculus is used will tell you almost everything you need to know about what I mean by currying. How do you "take multiple arguments" when you can only take 1 argument? Currying. This generalizes to other function-like things (like cfns) that may be able to literally take multiple arguments. We can still distribute the "curried" arguments among multiple function types. (But now we have more options about how to "take multiple arguments". And that's basically the problem.) None of this has to do with surface syntax or implementation techniques. If you think about how to implement cfns vs. lambda calculus functions efficiently, they are of course quite different. But type theoretically, they're not. >> >> 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. > > Right. And that has never been my intention. Not once. Not from the > beginning. Any time I have written an application in this style using more > than one argument it was my explicit intention that the arity of f was > unresolved in the absence of other information. In that case, I agree we have to say "maybe it's curried", which refers to currying. But I think we should not be writing cfn applications as if they were arity-abstract. >> 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. > > Unfortunately, that didn't clarify a thing for me. Bummer. Well maybe I'll try it again once we agree on terms for the apparently two meanings of "currying". _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
