On Thu, Mar 12, 2015 at 11:18 PM, Matt Oliveri <[email protected]> wrote:
> On Fri, Mar 13, 2015 at 12:57 AM, Jonathan S. Shapiro <[email protected]> > wrote: > > Matt: > >'m not sure why the afn types need to take an arity variable. > > Well in this case you're right, the arity variables don't say anything > interesting. But in choose_one, multiple afns would use the same arity > variable. > I still don't think arity variables are useful in choose_one, and I'm going to walk through that case concretely below. I think that in any case where they *would* be useful, the "call arrow" (the one I've been writing as '=>') solves this as well. > Another way to write this might be: > > > > a->b->c=>d->e->f=>r > > > > where the => arrows indicate required concrete call boundaries. This is a > > different (and I think, clearer) way of writing what I was trying to say > > with the "positional" idea. > > This notation is pretty nice. But are there actually multiple arrow > types there? For example, would it be parenthesized like this? > a->(b->(c=>(d->(e->(f=>r))))) > My intention was that the parenthesization should be a->(b->(c=>(d->(e->(f=>r))))) as you wrote above. As to whether it's a new arrow type, the answer is "yes and no". It is new in the sense that it provides an annotation of something that we weren't tracking before (the call boundary). It is *not* new in that the logic and type theory of the -> arrow apply equally well to the => arrow. 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. The annotation/effect intuition feels right in a behavioral sense as well. They accumulate in set-union fashion. So if unification occurs between two types a->b->c=>d->r a=>b->c->d->r the => always replaces -> in the result, giving: a=>b->c=>d->r This has the same consequence as the arity variable, without introducing heavy notation. Or at least: I think it does. I don't think that I'm stating the effect intuition correctly above, but it seems close. I'd kind of like to be able to wave my hands and say "well, this is just a sugaring for that effect intuition over there", because doing so would put us back into a known type theory. > If so, then it seems strange to change the "a->b->c =>" part to "cfn a > b c =>", as you propose below. I don't think it's strange, but It might seem more comfortable if I write it differently. From a type perspective, the substitution is between: a->b->...x->y=>r cfn a b ... x y =>r That is: we don't (on reflection) require a => on the LHS of the first type. In some sense, the => serves as a marker at which the two meeting types get aligned in column-like fashion. The stuff on the left and right of the => then "meet" recursively. But we could equally well write that as (a->(b->(c=>r))) cfb a b c => r That is: the parenthesis don't alter our ability to substitute. The crucial thing here is that we are cleanly substituting one syntactically complete expression for a second one. This mixed arrow notation does seem to solve the apply2 problem. But > it's not clear how it works for choose_one. For choose_one, we'd want > to enforce that multiple "a->b->c =>" groups have your rewrites 1 and > 2 above done to them in the same way, to get the same concrete > arities... Yes. And I *think* that the rule for substitution that I stated above does that. Let's work a concrete 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 Barring a typo, I think we can agree that these are mathematically identical functions with different concrete arities. That is my intent. 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. 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. Well, how about a case where an argument (therefore arity-abstract) function gets applied with different numbers of arguments in different places: def weird_apply f a b c { if random_true_false () let tmp = f a in tmp b c else let tmp2 = f a b in tmp2 c In this case we are applying the *same* function, so it's type unifies internally. Let's walk through this one with some care: The application f a leads us to infer the type 'a => 'b for f. The application f a b leads us to infer the type 'c -> 'd => 'e for f These two types unify, giving 'b =~ ('d=>'e) and therefore 'a => 'd => 'e for f. The application tmp b c leads us to infer 'f -> 'g => 'r1 for tmp The application tmp2 c leads us to infer ''h => 'r2 for tmp The type for tmp unifies with the return type 'b of f, giving: 'b =~ ('d => 'e) 'b =~ ('f -> 'g => 'r1) 'd =~ 'f, 'e =~ ('g => 'r1) typeof(f) = 'a => 'd => 'g => 'r1 The type of tmp2 unifies with the return type 'e of f, giving 'e ~= ('h=>'r2) 'g =~ 'h 'r1 =~ 'r2 All of this unifies with the argument variables, giving: 'arg_a =~ 'a 'arg_b =~ 'c 'arg_c = 'd And finally, we arrive at: weird_apply:: cfn ('arg_a => 'arg_b => 'arg_c => 'r) 'arg_a 'arg_b 'arg_c => 'r which is correct. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
