On Mon, Mar 30, 2015 at 9:59 AM, Jonathan S. Shapiro <[email protected]> wrote: > On Mon, Mar 30, 2015 at 3:29 AM, Matt Oliveri <[email protected]> wrote: >> On Mon, Mar 30, 2015 at 1:14 AM, Jonathan S. Shapiro <[email protected]> >> wrote: >> > I think the right thing to do for now is to write using AFN, and then we >> > can >> > go back later and figure out if a notation more similar to ML and >> > Haskell conventions is pragmatically tolerable. >> > >> > In order to discriminate your afns from mine in our discussion, I >> > propose >> > that you write the arity type variable as ?r rather than 'r. >> >> But, to be clear, the ?r is a deep arity variable? > > > Well, any notation that *has* an arity variable is your notation, so > presumably it should mean whatever you say it means. What *I'm* thinking for > *my* afn notation (which I'll write as 'safn' to reduce possible confusion) > is that > > safn a b c -> d > > is equivalent to what I have been writing as: > > a-?r1->b-?r2->c=>d
Oh OK. So you really do have your own version of afns now. Cool. (safn a b c -> d) seems like different notation for (a->b->c=>d), my mixed arrow-ized afn notation from a few exchanges ago. And I don't just mean they denote the same type, they really are just superficially different notations, since they both use elided callvars. >> I guess it's time to explain why (afn (?r1 ++ ?r2) 'a 'b -> 'c) and >> (afn ?r1 'a -> afn ?r2 'b -> 'c) are the same type. I think of "afn" >> as a type-level computation which ultimately reduces to some type >> formed with cfns. While the arity remains abstract, we cannot do the >> reduction, so we don't know what the cfns are, but because afn is >> "just" a total function producing a type, it must mean something. > > I think I agree that they are the same type; what I see here is merely a > difference in notation. It seems to me that in your notation it is less > visually obvious that a single input argument necessarily reduces to a cfn, > but that may just be a matter of getting used to the notation. To be clear, there is only one notation being used here: my original afn notation. For a given pair of variables ?r1 and ?r2 satisfying the appropriate constraints, (afn ?r1 'a -> afn ?r2 'b -> 'c) and (afn (?r1 ++ ?r2) 'a 'b -> 'c) are different ways of writing the same type in the same system, assuming we allow "++", which we probably shouldn't. The importance of these types being the same is that it explains why splitting the orginal afn with ?r is semantically just a matter of instantiating ?r appropriately. > The one I'm less convinced about is whether (your afn here) > > afn ?r1 'a 'b -> afn ?r2 'c -> 'd > > is equivalent to (your afn) > > afn (?r1 ++ ?r2) 'a 'b 'c -> 'd > > the thing that has been lost here is where the first arrow appeared in the > call chain. So this is a bit subtle, and it is a disadvantage, which is why I now prefer the mixed arrow-ized afns. If you could write "afn (?r1 ++ ?r2) 'a 'b 'c -> 'd" as a user, you're absolutely right that there is no intermediate call arrow imposed. But when we write "afn ?r1 'a 'b -> afn ?r2 'c -> 'd", it's implicit that ?r1 sums to 2. This is where the call arrow is hiding. In the scope of a certain ?r1 and ?r2 with the appropriate constraints, (afn (?r1 ++ ?r2) 'a 'b 'c -> 'd) and (afn ?r1 'a 'b -> afn ?r2 'c -> 'd) are the same type, even though the former way of writing it would not imply that ?r1 sums to 2. Basically we need to know about (afn (?r1 ++ ?r2) 'a 'b 'c -> 'd) to explain how (afn ?r 'a 'b 'c -> 'd) unifies with (afn ?r1 'a 'b -> afn ?r2 'c -> 'd). > The reason it matters is that two distinct applications can > cause us to need to preserve that knowledge at unification time. Given the > applications: > > f a b c > f d e > > it is still true that f is an abstract function type, but it is also true > that we need a => (a known-returning arrow) after both the second and third > arguments to the abstract function type. Yes. (I still like to call => a call arrow, since it's _not_ known-returning. It can diverge or throw.) > I'm not sure how this is captured in your approach? I tried explaining again. There must be a call arrow after two arguments because ?r1 sums to 2. So in this case (?r1 ++ ?r2) is either [2,1] or [1,1,1]. [3] and [1,2] are impossible because there's no way to take an ?r1 part that sums to 2. Yes this is an awfully indirect way to get the constraint. I prefer mixed arrow-ized afns now. But you asked about deep arity afns. >> The afn function takes a deep arity (with some obvious constraints), a >> list of argument types and a return type. So (afn ?r 'a 'b -> 'c) is >> sugar for something like (rawAFN r [a,b] c), where "rawAFN" is the >> actual function. > > As long as the arity is a deep arity, then I agree that it's possible to > encode chained afns (your afns) equally well with deep arities. I guess I > prefer to encode the affirmatively returning positions using an arrow, but I > think that's just a matter of differing aesthetics. I prefer being able to have a call arrow position too. This is what I did with the mixed arrow-ized afns. We can explain that in terms of a rawAFN function too. It takes a list of bool instead of a deep arity. The constraint on the list bool is simply that its length is one less than the length of the argument list. We use a helper function to accumulate arg types for a cfn: rawAFN' acc [] [tp] rtn = rawCFN (rev (tp :: acc)) rtn rawAFN' acc (true :: p) (tp :: args) rtn = rawCFN (rev (tp :: acc)) (rawAFN' [] p args rtn) rawAFN' acc (false :: p) (tp :: args) rtn = rawAFN' (tp :: acc) p args rtn rawAFN p args rtn = rawAFN' [] p args rtn >> It's defined recursively: >> >> >> rawAFN [] args rtn = rtn // That weird base case >> rawAFN (a :: r) args rtn = rawCFN (firstn a args) (rawAFN r (skipn a args) >> rtn) >> >> Oh yeah, rawCFN takes a list of argument types and a return type. > > > I *think* I understand what you are saying, but it's not obvious to me how > this addresses the unification case I have just described above, where we > can't decide how the first two arguments are consumed based on the > applications we can see. *Because* we can't decide, I think we're still > dealing with an abstraction function where those two arguments are > concerned. The consumption of the third argument (c) can be converted to CFN > because *all* single argument functions can directly be converted to cfn. I hope I have answered this. >> The constraints on the deep arity argument of rawAFN are: >> - Each element is an integer > 0. >> - The sum of the elements is the length of the list of argument types. > > Those constraints make sense, but they don't seem to address my unification > example. But here's a better example. Suppose we see applications > > f a b > f a b c d > > then it seems to me that your type will be something like > > afn (?r1 ++ ?r2) a b c d -> ret > > but we have lost the information here that ?r1 and ?r2 must each account for > two of the arguments. How is that captured in your proposal? No it would just be afn ?r1 a b->afn ?r2 c d->ret The list append business is internal machinery. >> I'm not sure yet if >> we'll actually ever need to write "++" or "::" for arity lists either. >> Mixed arrow notation suggests that we will not. > > I'm actually not fond of the mixed arrow notation. It's useful in the > present discussion to clarify things, but I think it will introduce > surprises. I have a thought about what to do, but it's going to produce an > argument here, and I'd like to do *that* argument separately from this > argument. I mean I think you're right that we'd only need to write -y-> arrows and -?r-> arrows, which suggests that with deep arity afns we'd never need to write constructed deep arity expressions, just variables. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
