On Thu, Mar 12, 2015 at 4:55 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Wed, Mar 11, 2015 at 2:34 PM, Matt Oliveri <[email protected]> wrote: >> On Wed, Mar 11, 2015 at 2:55 PM, Jonathan S. Shapiro <[email protected]> >> wrote: >> > On Tue, Mar 10, 2015 at 5:26 AM, Matt Oliveri <[email protected]> wrote: >> >> >> >> 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. >> >> Yes, it's OK that f's type is arity-abstract, but that's not the >> issue. Your type for apply2 is wrong. The f apply2 receives needs to >> accept at least 6 arguments (across an unknown number of >> applications). >> >> apply2 :: cfn [a->b->c->d->e->f->s] => s > > Oh. I see my mistake now. What you are saying is that f has to be some > [sequence of] call[s] that consume the three arguments "1 2 3" and then > returns a function that in turn [possibly through a sequence of calls] > consumes 4 5 6. So yes, in that case, I agree that your abstract function > type is correct, and therefore that the type you give for apply2 is correct. > > Which is problematic, because we have somehow lost our knowledge of the fact > that f must ultimately concretize to something that involves a => arrow > after the third argument.
Exactly. > And we can't express this with the list-like cfn arity notation, because > that doesn't give us the right kind of expressiveness. We need a way to say > that there must be a => arrow after the third argument to f, without saying > how many => arrows precede that one. Right, but that wasn't what the list arity was supposed to do. In my deep arity scheme, the list arity (deep arity) describes a certain way of instantiating a "group". The groups themselves capture the max shallow arity constraints. Writing a group as an "afn" type (which you had a problem with before, but maybe you're warming to two function types), the type of apply2 would be: cfn (afn ar1 a b c->afn ar2 d e f->s) -> s afn's are for arity-abstract function types. The "afn" part is a keyword, the next thing is the deep arity (which are variables in both afns above), then zero or more (Yeah, zero. That wonky base case. No one will type in base cases.) argument types, a "->" token, and finally the return type. Notice that one afn is the return type of another. That's the key thing to exploit: we can nest afns to group arguments without fully specifying the call arities. So we've broken the problem of concretizing the type of f into concretizing two groups of will-be cfns, one for each afn. ar1 and ar2 are instantiated independently, as you'd hope from the syntax. Each one must be a deep arity whose elements sum to 3, the number of arguments for the relevant afn. Each one indicates the way an application should be specialized as one or more calls. There are probably a lot of questions you have about how afn types would work in various cases, and I've sort-of answered them back when we weren't understanding each other. But basically, for now I think I've said enough that you can see how grouping solves the apply2 problem. The deep arities solve the choose_one problem. > If I take this as a constraint problem, then it's fairly easy to have a > compiler-implement pseudo type-class to handle this. E.g. we can imagine > type classes named =>1, =>2, =>3, and so forth, and then qualify the cfn > type with one or more of those to say where => arrows must appear. It does > not seem a huge leap to imagine that we could come up with a more > syntactically convenient way to say that. I can't visualize this yet, from what you're saying. I don't want to be bossy, but maybe you could consider my schemes before inventing another. It might be easier. > What this *seems* to suggest is that (as you have been saying) arity-lists > aren't as simple as I have assumed. I now wonder if a better way to think of > an arity list (note new notation) <1, 3, *> is to read that as "an => arrow > must occur after the 1st and 3rd arguments". If we wish to be flexible about > what happens after the 2nd argument, we would write it as <1, *, 3, *>, or > something of that sort. But I think the right intuition here is that we are > accumulating constraints on the acceptable types of /f/ > > Does this seem more workable? Well right now, I still like my way. I don't yet understand the meaning of your notation in general. BTW, the new arity list notation here doesn't seem to be like my deep arities, in either form or function. So there's potential for confusion if we just call things arity lists. >> I agree that either arrow token will probably turn out to be >> unambiguous, due to the cfn. But I prefer "->" because then it's >> easier to see functions at a glance. > > I agree, or I did until I was forced to suggest the new arity list approach > above. I still think this is cleaner, but we may want to hold on to a > distinguished arrow in the present conversation. Well, I'm going to use "->" for my deep arity scheme. I'll use whatever you want for your schemes. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
