Responding from a park bench; please forgive brevity. 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: > > Separately, I have a gripe with framing the choose_one problem as that > some types must unify. I understand, and to some degree I agree. When we speak of unification, we often mean (implicitly) that we are using an HM-style system in which unification is the main mechanism of resolution. In this case, however, the types are "joined" (or, if you prefer, are required to be equal) by the return statement. Whatever mechanism we use to resolve and check the types, unification is a reasonable way to capture this sort of type equivalence. > >> > 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. > > 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. 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. 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. 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? 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. > > I see no reason to think that the chaining of calls in this example makes > > that any more difficult than it was before. > > How about now? > Well, it's a lot easier to see now that I understand that I can't read. :-) shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
