Pal's timing is excellent, as I was mulling parallel thoughts. I was thinking that we need notations to distinguish concrete function calls from applications, and that one of the problems in our conversation has been a failure to adequately distinguish these syntactically. 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.
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". 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. 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. 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. 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. What am I missing, and what further points do we need to cover on this? shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
