On Tue, Mar 10, 2015 at 1:45 AM, Jonathan S. Shapiro <[email protected]> wrote: > I'm not entirely > convinced that we need a different arrow here. It seems to me that "=>" is > already taken for constraints, and perhaps the presence of square brackets > is enough to tell us which arrow we are dealing with.
So the thing you call is a concrete function, and the thing you apply is an arity-abstract function? Well we don't want to write arity-abstract function types exactly same way as concrete function types, or I'll probably never get what unification is doing. > I am mildly confused about one point, which is the relationship between > call[s] and application[s]. In particular, given > > f a b c > > there several possible arrangements of calls that might implement this, one > of which is: > > f [a] [b] [c] > > So my question is: is "f a b c" one application or more than one? I'm hoping > (and I believe Pal intended) that the answer is "one". If an arity-abstract function type is inferred for f from "f a b c", then I agree it should be considered one application. > I also agree quite strongly with Pal that functions have arity and > applications do not. That's consistent with the use of the term "arity" in > the literature, and I'd like to stick to that. As long as calls still have arity, I can deal. If not, I need to know what to say instead of "arity-n call" or "n-call". > The other thing I've been thinking about is this question of arity-as-list. > Going back to the example above, > > f a b c > > has several possible realizations as function calls: > > f [a] [b] [c] > f [a b] [c] > f [a] [b c] > f [a b c] > > So I'd propose as a base case that when a function does NOT return a > function-valued return value, then it's arity should be expressed as a > single-valued list. E.g. > > def g x y = 1 // arity [2] > > if a function g returns a value of concrete function type /cft/, then the > arity list for g amounts to > > nargs(g) :: arity-of(cft) // where :: is, in effect, "cons". > > The principal that we concatenate nargs(g) with the arity of g's return > value, and treat a non-function-valued return value as the empty list, seems > to hold up pretty well here. In > > def g x y = x > > the arity list for g is > > nargs(g) :: arity-of(x) > > > There may be a cleaner way to think about this, but I provisionally believe > that we can treat arity-of() as a type-level accessor that returns list(Nat) > for concrete functions and is treated similarly to an unresolved type > variable for abstract function types. This definition makes sense to me, and matches how I explained deep arity at first. But I later decided it might not be so useful to really have deep arity go all the way down to a known non-function type. It seems more useful to be able to talk about "deep" arity relative to any chosen return type, which may be a type variable, and thus, possibly a function type. The reason is that what I wanted deep arity for is to distinguish different arity instantiations of an arity-abstract function type, but if arity-abstract function types can be nested, then we expect the return type to sometimes be a function type, and deep arity is about the arguments before we get to that function type. That is, the arguments handled by the outer arity-abstract function type. > And finally, the type rule requirement at an application is that the number > of arguments present must be an exact match for the list-wise sum of the > shallow arities of the function calls that implement the application. Yes, but that seems to be saying it kind of backwards, since, looking at an application, we get to pick the shallow arities of the function calls, not the number of arguments. (Ah ha! You said calls have arities!) Maybe I'm jumping the gun and you're just saying how to check an application against curried concrete function types. But that should fall out of the behavior of arity-abstract function types when we have them. Seems to me applications are a sort-of elimination rule for arity-abstract function types, so we should introduce the two simultaneously. > The piece that seems to be missing here is to resolve the problem that was > identified for choose_one. Offhand, it seems to me that the rule should be > that unifications must be preserved when applications are rewritten to > calls. I don't follow that. Can you pick a notation for arity-abstract function types and show how the choose_one example gets checked? > What am I missing, and what further points do we need to cover on this? Just to address the grouping issue. Here's an example where I think we want grouping: def apply1 f = f 1 2 3 def apply2 f = apply1 f 4 5 6 Any alternative explanation of how this is handled would also help provide a common understanding of the issue. I am OK if it turns out apply2 needs to be written as def apply2 f = (apply1 f) 4 5 6 (That doesn't seem to alleviate the need for grouping though.) _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
