On Wed, Feb 25, 2015 at 9:03 AM, Jonathan S. Shapiro <[email protected]> wrote: > On Tue, Feb 24, 2015 at 11:25 PM, Matt Oliveri <[email protected]> wrote: >> But this doesn't explain why you said that argument positions can >> concretize as certain arities. > > I think you are reading too much into my wording.
Yeah, probably. > Let's see if I can say it > a different way: > > Once > > fn 'arity 'a->'b->'c->'d->'r > > > unifies with > > fn 1 'u->'v > > > we know that the result type 'v must be: > > fn 'newArity 'b->'c->'d > > > which tells us that the first function, when applied, will return a second > function. Mathematically you might be able to compose these two functions to > arrive at a third. Programatically you can only perform their applications > in sequence. > > So all I'm saying is that this result function has an arity-abstract type > that will (in turn) be unified and specialized, and will eventually turn > into an arity-concrete function type. The particular arities I gave were > wrong, because 'd could unify as a function type at some point. > > I suspect we are merely hung up on a notational issue. For convenience of > discussion, we have been assuming (in next example) that 'r will not end up > being a function type, and therefore that: > > fn 'arity 'a->'b->'c->'c->'r > > > might possibly end up having deep concrete arity [1, 2, 1], But of course no > concrete function will actually end up with arity [1, 2, 1], because all > concrete function arities have a depth of exactly 1. What we will end up > with instead in this case is *three* concrete functions. The first will have > arity 1, the second arity 2, and the third arity 1. It doesn't seem like you're saying anything I didn't know here, and this time you didn't talk about arities of argument positions, so I guess it was nothing. >> On Wed, Feb 25, 2015 at 12:28 AM, Jonathan S. Shapiro <[email protected]> >> wrote: >> > My choice of notation for function types is not innocent. The [shallow] >> > concrete arity corresponds to the stuff up to, but not including, the >> > return >> > type. >> >> This is not necessarily true. Well, it is if you interpret "return >> type" with care. Maybe that's what you're saying. In (fn 'arity >> 'a->'b->'c) we do not know what the return type is. It isn't >> necessarily 'c, because if 'arity is 1, then the return type is >> something like (fn 'newArity 'b->'c). > > Indeed we do not, and that is precisely why we have written 'arity rather > than some natural number. Please note that in my sentence above I said "the > shallow **concrete** arity". Ah. In that case, what you said seems rather obvious. But thank you for ensuring that I wasn't confused by this. >> > This leaves the return type to unify in abstract form, just as it does >> > when 'c unified with 'w->'x. >> > >> > The part of this that needs some care in explaining is how the Nat >> > constrains the unification. In particular it needs to account for why >> > >> > fn 1 'a->'b >> > >> > cannot unify with >> > >> > fn 2 'a->'b->'c >> > >> > because the number of [transitive] shallow argument positions cannot be >> > reconciled. >> >> This explanation doesn't seem to have anything to do with the axiom of >> choice, or how 'newArity got there. > > You are right. I said "axiom of choice", but I was thinking about > permutations. Somehow I turned "n choose k" into "axiom of choice" in my > head for a moment. Please forget my axiom of choice brain-fart. Sorry about > that. Thank goodness. That would've been weird. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
