Hi, It seems to me that you are confusing the rather abstract “application” from functional languages and what I call a (function) “call”.
Would it perhaps be better to use [] brackets to indicate C-like calls. In other words: f [a b] is a call to a function f by two arguments. f a b simply means the application of f, a and b. It could mean either 1) f [a b], or 2) f [a] [b] <=> (f [a]) [b], or 3) any eta-expansion of the application (the eta-expansion rule is [\x . f x <=> f]). Applications do not have arity. Calls do have arity. We can only talk about arity when an application has been translated to a number of calls. Does this help? PKE From: bitc-dev [mailto:[email protected]] On Behalf Of Jonathan S. Shapiro Sent: Tuesday, March 03, 2015 12:16 PM To: Discussions about the BitC language Subject: Re: [bitc-dev] Arity, Take N On Tue, Mar 3, 2015 at 11:45 AM, Matt Oliveri <[email protected]<mailto:[email protected]>> wrote: On Tue, Mar 3, 2015 at 10:46 AM, Jonathan S. Shapiro <[email protected]<mailto:[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. Arity is a property of the function being applied, not a property of a [potentially progressive] application. What I mean by "progressive" here is that the n arguments present need not be consumed by the leftmost application. 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. 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). 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. 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. (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. I have no idea why we are talking about curried applications of cfns. What in tarnation does that mean? By the time a cfn is introduced, any ambiguity about number of consumed arguments should be explicitly resolved. >> >> > 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. 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. 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. 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. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
