On Fri, Feb 27, 2015 at 4:58 AM, Keean Schupke <[email protected]> wrote: > I see your point, however do we ever require arities to match exactly? You > can always supply more arguments to a curried functions (up to the > max-arity) without allocation, so we only need a "minimum arity" for any > function.
Yes. The native calls will require arities to match exactly. Any wiggle room for arities is something that has to be provided by the compiler somehow. We both think we know a way to provide this. In broad terms, we agree that we can apply more arguments than the native arity calls for, resulting in a sequence of function calls. We also seem to agree that we can't do the opposite and apply fewer arguments than the native arity calls for. However, when it comes to making this precise, we disagree about how much can be reasonably allowed. In particular, I think making higher-native-arity functions supertypes--in the usual sense of subtyping, using a subsumption rule--allows programs that would require too much magic to implement without implicit allocations. The implicit upcast example I keep emphasizing is pointing out the basic flavor of the cases I see as problematic. The key is that subsumption allows the arity to be _implicitly_ upcast anywhere. Of course coding your own explicit upcasts using explicit lambdas is OK, subtyping or not. In order to convince me that you have a solution to this case, you have to start with what we can take for granted, which is calls where native arities match. We agree that we can do better, but we don't agree _how_ to do better, and whether an arbitrary implicit upcast can be handled. So you can't assume we can do any better than exact matching when you explain how your proposal will implement my implicit upcast. > We already know the 'maximum arity' as this is the fully-curried > arity which is implicit in the type already. Not necessarily, as Shap has been carefully pointing out. We don't know the maximum total arity of a curried function until it concretizes enough for us to find the final, non-function-type return type. > Even with the casts, I dont see a problem with this: > > cast2_to_1_1 :: (fn 2 'a -> 'b -> 'c) -> fn 1 (fn 1 'a -> fn 1 'b -> 'c) > > ((cast2_to_1_1 f) 'a' 'b') First of all, that's a downcast. I am asking about an upcast, since that's what is provided by subtyping. Second of all, you're explicitly applying some already-implemented cast. Of course there's no problem with that. Indeed, that code already works when native arities must match. But that isn't the problem. How do you implement the upcast in the first place, when it's written as I wrote it, without any explicit coercing of the argument? At the risk of being so clear as to insult your intelligence, I _know_ we can upcast on-the-fly when we apply a function. Shap's proposal does essentially that. I _know_ we can upcast on-the-fly when we _define_ a function. My proposal does essentially that. But your proposal promises more. It says the upcast is a stand-alone, implicit operation that can be lifted to a function, as my (upcast2to1_1 f = f) does, and called without restriction. In other words, you've lead me to believe that the implicit upcast in my definition of upcast2to1_1 is allowed in your proposal. How does _that_ work?? In case it wasn't clear, even if you think of arity-abstract definitions/applications as on-the-fly implicit upcasts, so that Shap's and my proposal allow _some_ implicit upcasts, we do not allow the implicit upcast I used in upcast2to1_1. To understand why not from an implementation point of view, it's because you need a lambda, there's nothing around to inline it into, and it escapes. To understand why not from a type theory point of view, it's better not to think of our proposals in terms of subtyping; thus, there's no reason why it _would_ be allowed. > On 24 February 2015 at 17:00, Matt Oliveri <[email protected]> wrote: >> >> On Tue, Feb 24, 2015 at 10:37 AM, Keean Schupke <[email protected]> wrote: >> > On 24 February 2015 at 15:33, Keean Schupke <[email protected]> wrote: >> >> On 24 February 2015 at 15:30, Matt Oliveri <[email protected]> wrote: >> >>> >> >>> upcast1_1to2 f = \x y.(f x) y >> >>> downforce2to1_1 f = \x.\y.f x y >> >> >> >> Why is that necessary? >> >> >> >> If this is true then you cannot go up or down, so there is not point in >> >> arty-abstract functions at all, as you cannot alter the arity without >> >> inserting lambdas. >> > >> > There is definitely some weird assumption here, like you are trying to >> > define a coercion to fit into an existing type system or something. You >> > are >> > tying to define a unary coercion that can be used like this: >> > >> > f (upcast1_1to2 g) >> > >> > But that is not at all what we are doing here. There is no need for the >> > coercion to be a unary funciton, remember that both 'f' and 'g' are >> > still >> > arity-abstract in the implementation, so we can specialise them iff they >> > pass the subtyping test. >> >> For some reason, I received this email later than your more recent ones. >> >> The coercion needs to work in a system where arities must match >> exactly, since--as I understand it--your proposal is relying on them >> to provide arity subtyping in the first place. To assume arity >> subtyping or similar when implementing the coercions would be begging >> the question. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
