On Fri, Mar 13, 2015 at 2:14 PM, Matt Oliveri <[email protected]> wrote:
> On Fri, Mar 13, 2015 at 11:06 AM, Jonathan S. Shapiro <[email protected]> > wrote: > I was starting to think so. Your mixed arrow scheme is actually quite > different from my deep arity (cfn/afn) scheme then. > I still don't understand your deep arity scheme. > > One way to think about the => arrow is that it is really a -> arrow with > an > > attached annotation. Another way to think about it is that it is -> arrow > > with a "no-implicit-closure" effect attached. That is: if a -> arrow > > survives to be "executed", it will need an implicit closure construction, > > while a => arrow will not. > > Errm, that's a weird way to put it. We never allow implicit closures. > Yes and no. I would say that our *goal* is to avoid implicit closures, and that the reason we are talking about mixed arrows and/or deep arities is to determine how to accomplish that restriction. > Whatever kind of constraint it is, constraints are generally not > enough to guarantee abstract types will concretize the same. You can > get lucky sometimes, and you did get lucky, as I'll explain. > Hey! choose_one was *your* example! :-) > > def f1 a = lambda b c { 1 } // cfn int => cfn int int => int > > def f2 a b = lambda c { 1 } // cfn int int => cfn int => int > > def f3 a b c = a // cfn int int int => int > > Well it kind of looks like f1 and f2 always return 1 while f3 returns > its first argument. > Yes. My mistake. f3 should be returning 1. My intention was to do three versions of the same computation differing only in their native arity. > > Now lets look at pseudo-code for choose_one: > > > > def choose_one x y z { > > if random_true_false () > > x > > elseif random_true_false() > > y > > else > > z > > choose_one:: cfn 'a 'a 'a => 'a > > > > > > And now let's look at the type resolutions when we try to call this as > > > > choose_one f1 f2 f3 > > > > > > Note that there exists *some* order in which the formal parameter types > > "meet" and are checked/resolved against the actual parameters. Choosing > > arbitrarily, lets check f1 =~ x first: > > > > cfn int => cfn int int => int =~ 'a > > > > > > so now we have 'a = (cfn int => cfn int int => int), and we check > > (arbitrarily) f2 =~ a next: > > > > cfn int int => int =~ ('a = (cfn int => cfn int int => int)) > > > > > > These two types are not compatible, so the application (correctly) fails > to > > type check. In fact, this is what has puzzled me about the choose_one > > example; it has always seemed to me that the argument types unify and so > > there can be no failure to detect concrete incompatibility at > > specialization. > > Shap, this example is way too easy. Of course if you have > arity-concrete function types, it'll work out. That is not in any way > a test of your arity-abstract function types. Here's the example I > think you meant, which still happens to work, because you're lucky: > > The f's are unknown functions with arity-abstract types: > f1 : int=>int->int->int > f2 : int->int=>int->int > f3 : int->int->int=>int > No. This is most definitely NOT the example that I meant, because this is (or should be) impossible in my scheme. All function definitions assign a concrete arity. Therefore, a passed function must, of necessity, have concrete arity. If that isn't true then my entire approach breaks down. I want you to pause here, and try to explain to me how, in a language where all function definitions assign concrete arity, it is possible for f1, f2, f3 to end up with abstract function types in the way that you describe above. I can certainly see how this might occur while the functions are still abstract. But by the time they are concretized I think this should no longer be possible. > When we pass them to choose_one, the instance of choose_one's type becomes: > cfn (int=>int=>int=>int) (int=>int=>int=>int) (int=>int=>int=>int) -> > (int=>int=>int=>int) > > because we combine the stricter => arrows which variously appear in > each position. Well (int=>int=>int=>int) is actually arity-concrete > after all; it's the same as > cfn int=>cfn int=>cfn int=>int > > So we're OK. f1, f2, and f3 must turn out to have that concrete arity. > Right, and I don't think that's an accident, though I haven't read below yet (I'm responding linearly). > Where you get in trouble is whenever the constraints don't happen to > add up to a concrete arity. Example is coming up. > > > I think it's also interesting to look at apply_one. Reusing f1, f2, f3 > from > > above, here is apply_one: > > > > def apply_one x y z a b c { > > if random_true_false () > > x a b c > > elseif random_true_false() > > y a b c > > else > > z a b c > > apply_one:: cfn ('a->'a->'a->'r) ('a->'a->'a->'r) ('a->'a->'a->'r) 'a 'a > 'a > > => 'r > > > > This case is interesting because the three function argument types do NOT > > unify. And *because* they do not unify, the application > > > > apply_one f1 f2 f3 1 2 3 > > > > type checks (and specializes) correctly, which is what we want. > > I agree. With afns too, x y, and z would not get unified. So each afn > would each have a fresh arity variable inferred for it. Here's an > example that's really funny because in HM it'd be functionally > equivalent to apply_one, but the function types do unify, and this > means that it's not even the same type in BitC. > > def not_apply_one f1 f2 f3 a b c = (choose_one f1 f2 f3) a b c > > See there's only one application to specialize. Oh well. The thing > that's so funny about this example is that it's also the example that > breaks your scheme. > > Here's the type I'd give it: > not_apply_one : cfn (afn 'ar 'a 'b 'c->'r) (afn 'ar 'a 'b 'c->'r) (afn > 'ar 'a 'b 'c->'r) 'a 'b 'c -> 'r > > The three function arguments must have the same arity, as you can see. > > Here's the type I suppose you'd give it: > not_apply_one : cfn ('a->'b->'c=>'r) ('a->'b->'c=>r) ('a->'b->'c=>r) > 'a 'b 'c => 'r > > You (correctly) do not infer an arity-concrete type for f[123], since > there is no reason to do so. But what's wrong with that type? Well, > AFAICT, the arguments do _not_ need to have the same arity! We can > instantiate each one separately, like: > cfn (cfn 'a 'b 'c=>'r) (cfn 'a 'b=>cfn 'c=>r) (cfn 'a=>cfn 'b 'c=>r) > 'a 'b 'c => 'r > > Now we use functions of different arities for f1, f2, and f3. Oops. > Let me start with a question. You wrote "AFAICT, the arguments do _not_ need to have the same arity!", but I am not clear which function you are referring to here. If you are referring to choose_one, then my answer is: yes they do, because all of those types meet at the return type. A consequence is that no, I would NOT type not_appply_one in the way you suggest. Something went wrong here, and it is the reason I wanted to appeal to an effect-like intuition about the arrows. My originally given type for choose_one was: cfn 'a 'a 'a => 'a You went and substituted ('a->'b->'c=> 'r) through for 'a on my behalf, which is perfectly good as a term substitution in HM, but it's no good here. The reason it's no good is that the identity-of-types requirement has been lost in the substitution. The reason that happened is that this way of writing the type is conceptually incomplete. The reason it is incomplete is that you have omitted the effect type variables on the arrows. Once those are restored, the necessary identities will once again be preserved. I can't write this using your notation, because the afn notation doesn't say what I need. I think the *correct* substitution of an abstract function type here would be to substitute 'a -a1-> 'b -a2-> 'c => 'r for the 'a parameter type in my typing of choose_one. By unmasking the effect variables, it becomes clear that all of the arities have to go in positionally correlated ways. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
