On Fri, Feb 20, 2015 at 1:24 PM, Matt Oliveri <[email protected]> wrote:
> On Fri, Feb 20, 2015 at 10:34 AM, Jonathan S. Shapiro <[email protected]> > wrote: > > On Thu, Feb 19, 2015 at 11:16 PM, Matt Oliveri <[email protected]> > wrote: > > > >> > >> So if we start with > >> fn arity a->b->c->d->r > >> > >> and we want call it with two arguments, you say we get > >> fn 2 a->b->c->d->r > >> > >> ...There's still a choice of native arity to be > >> made. So I propose it should really be written: > >> fn a b -> fn newarity c->d->r > > > > > > Yes. Sorry. That's correct, and with the arity variable made explicit > that > > is how it should be written. > > Well, I don't understand. If (fn 2 a->b->c->d->r) isn't really right, > then the notation isn't really right already with a constant arity. > I'm thinking this is probably clarified by now, but just in case.... Rewriting this using the full (unelided) notation, we would be specializing fn arity a->b->c->d->r with fn 2 a b -> fn newarity c->d->r I think the confusion above comes from one of my convenience syntax proposals, which was that we could choose to read 'a -> 'b -> 'c as a convenience syntax for fn 'freshArityVariable 'a -> 'b ->c If we adopt that convention, then our reading of fn 2 a->b->c->d->r would be fn 2 a ->b -> fn 'freshArityVariable c->d->r Making the arity a variable cannot help, right? I was trying to > illustrate something weird by trying to use the arity variable > notation, but really I don't understand it. > The arity variable is a type variable having Nat kind, which means that is has to specialize to a natural number. > The original reason I was suspicious of definitions always being > concrete was an example that looked kind of funny that way: > > passArith f = f (\x y -> x + y) (\x y -> x - y) > passArith : fn ((fn Nat Nat -> Nat)->(fn Nat Nat -> Nat)->Nat) -> Nat > > So this function has a concrete arity, its parameter is > arity-abstract, and its parameter's parameters have a concrete arity. > This seemed weird. However, it seems to work: > Yes. > Since your scheme worked better than I expected here, I figure you > should be the one to explain the reason for concrete definitions, and > perhaps reasons against other schemes. > It comes down to something simple: we need to get a concrete arity from *somewhere* for both calling convention and interoperability purposes. The only place we can really establish that is at definition/declaration. The reason to infer arity at applications is that it (a) it reduces the likelihood of library bifurcation for human reasons, and (2) there are some useful constructs in functional languages that are syntactically very awkward when a concrete-arity-mandatory application syntax (as in Pascal) is adopted. The place we care about flexibility is at the use occurrence. All of the optimization advantages Keean is contemplating can still be had by the optimizer in the presence of arity-concrete definitions. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
