On Tue, Mar 10, 2015 at 5:26 AM, Matt Oliveri <[email protected]> wrote:
> On Tue, Mar 10, 2015 at 1:45 AM, Jonathan S. Shapiro <[email protected]> > wrote: > > > 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!) > Whether it's backwards or forwards, the rule still holds. Arguments present at an application need to be consumed. The [potentially abstract] function type guarantees that we won't type check if too many arguments are present. The issue I'm actually getting after here is that we can't be building hidden closures either. > > 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? > Well, no. At the moment, I can't, and that's more or less my point. What I'm trying to say here is that given choose_one x y z // returns (randomly) one of x, y, or z then typeof(x) ~= typeof(y) ~= typeof(z) where "~=" means "unifies with". That unification must hold whether typeof(x) is concrete or abstract. The problem I'm trying to identify here is that I don't (yet) have a rewrite strategy that guarantees this unless we do something like the list-like arity notation. > > 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 > So I'm not sure why this creates a special need for grouping **in the types** beyond what is already needed for function parameters generically. If function definitions produce concrete functions, then the types above would seem to be: apply1 :: cfn [a->b->c->r] => r apply2: :: cfn [a->b->c->r] => r That is: we won't know the concrete call bracketing used by f until we see an instantiation of apply2 (or apply1), and that's perfectly OK. Note that I'm attempting to use Pal's notation here, but I may not have gotten it right. Personally, I think that the square braces convey nothing new in cfn types, because cfn a b => r seems sufficient to describe concrete arity at a definition. The place where the square brackets seem useful is in describing how an application gets concretely implemented by particular calls. Pal: do you agree that square braces aren't useful here if we retain the "cfn" token? Matt: assuming that the "cfn" be explicitly present when writing this type, do you feel that the arrow is sufficiently disambiguated by context, or would you prefer to stick with Pal's => arrow for now? I think that we will eventually we will need to replace it because of the constraint arrow, but perhaps the => arrow is sufficiently disambiguated by "cfn" as well. E.g. the following is not ambiguous: add :: arith 'a => cfn 'a 'a => 'a 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 I don't think that should be necessary. The entire point of the current discussion is to determine how to re-write correctly from apply1 f 4 5 6 // what the user wrote to apply1 [f] [4 5 6] // how we re-wrote it I see no reason to think that the chaining of calls in this example makes that any more difficult than it was before. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
