On Fri, Feb 13, 2015 at 12:35 PM, Keean Schupke <[email protected]> wrote:
> > Given your proposal, consider a function using curried application that >> has been constrained by a NOALLOC effect. Does an algorithm exists that is >> guaranteed to perform curried application without any allocation, in the >> case where the function being applied cannot be statically resolved, and so >> we cannot guess the function's native arity given that you propose it >> should not be encoded in the type? >> > > The compiler would pass the import and store two type signatures for the > function, the native-type and the 'local-type'. The program would initially > be type checked with the local-type, then optimisation passes applied, then > type checked again with the native-type, and fail this type check if it has > been unable to solve the uncurrying (or it can add thunks if allowed). > I don't think that works. If we take the position that implementation and type should be firmly separate, then when I see a function in a module signature, how do I know it's arity? It's possible that you are assuming the F# approach here, but note that their approach *also* avoids placing arity in the type. It appears to rely on seeing the definition of the function. So in their scheme, if I can see def f x y = x + y f : 'a -> 'a -> 'a I know that's a function with arity 2. But if I merely see 'a -> 'a -> 'a (which is what I would see at a module boundary declaration), I don't have the arity information. The issue is even more apparent when you consider the def f x = fun y -> x + y example they gave, which apparently gets assigned arity 2 in their scheme by unspecified means. I'm not saying that arity has to be associated with type. I'm saying that it has to be associated with *something*. And it really *appears* to me that it has to be associated with type, because if it isn't, there seem to be a whole lot of ways that the two can get separated and also a whole lot of places (e.g. function parameters) where there is no way to convey the needed information. In this sense, OCaml and Haskell are cheating. It's not that they don't encode arity in type. It's that they do it by assigning arity 1 to all functions. > I cannot prove it is possible, but I have a hunch that by AST manipulation > you can always solve the uncurrying problem. The idea is that the function > must be applied to both arguments at some point, so we just need to bring > the arguments together (this assumes purity) by reordering the code. I > think beta reduction would work. imagine: > > inc x = add 1 x > > f x = inc x > You have made a number of arguments of this form during this thread. A consistent flaw in those arguments is that you have relied (perhaps unintentionally) on the ability to statically resolve the procedures. I agree that you can do the term substitution you propose in your example above. Please explain how to do the comparable term substitution in the body of the following function: def f (g : 'a -> 'a -> 'a) x = g x Note that all you have for g here is it's type, which (per your desire) does not convey arity. We know enough to apply g to x. We don't know enough to know whether that application allocates or not. This is true because we don't have enough information to know whether it is a partial application. Stepping *down* a level of abstraction here, let's think about the optimization that does closure elimination. So we have something like: def myAdd x y = x + y and an expression myAdd y v // which in curried form is really (myAdd x) v Good so far. And now we'll fiddle with some region types to get the closure record for the (myAdd x) part lifted into the parent stack. Still good. And having done that we're going to rewrite the expression into an application of an arity-2 version of myAdd, whereupon we can apply dataflow and eliminate the closure record. All of this we can do, except for one crucial thing: in an arity-less type system, we have no way to type that intermediate myAdd in a way that tells us it has arity 2! One of the things we tried in BitC v0 that was a huge success was to keep the type system all the way down. It did wonders for catchiing mistakes. If you want to do that (and I do), the optimization sequence above requires the ability to capture arity in type. I would again want monadic effect control so all 'application' arrows are > pure... > Until somebody explains to me how to reconcile monads and concurrency, we can't go there. Even if we *can* explain that, there are still concerns about monad composability. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
