On Tue, Feb 24, 2015 at 10:19 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Tue, Feb 24, 2015 at 6:44 PM, Matt Oliveri <[email protected]> wrote: >> >> On Tue, Feb 24, 2015 at 7:47 PM, Jonathan S. Shapiro <[email protected]> >> wrote: >> > On Mon, Feb 23, 2015 at 12:57 PM, Matt Oliveri <[email protected]> >> > wrote: >> >> Before I forget, another question I have about the notation is how to >> >> read off the maximum arity when the return type is a variable. >> > >> > You can't, because the maximum arity (which I take to mean the sum of >> > the >> > list elements in your lists] is underspecified until the return type is >> > concretized. It can become sufficiently specified sooner, but there is >> > no >> > guarantee that it will. >> >> Well maybe there's some subtlety to your proposal that I missed, but >> here's my take: >> >> No, the maximum arity is the maximum shallow arity of functions that >> can unify with it. It's inferred from the number of arguments applied. >> So like: >> f 1 2 >> we infer f has type (fn 'arity Nat->Nat->'a), right? But the maximum >> arity is 2. We cannot unify with (fn 3 Nat->Nat->String->Float) >> because then (f 1 2) was a partial application, and allocates a >> (String->Float). But it sure looks like we can. >> >> In other words, I assumed your arity-abstract function types always >> have maximum arities, but your notation didn't make them unambiguous. > > The *shallow* arities always have a concrete answer, which is part of why I > prefer to think of this as a shallow (i.e. leftmost) > specialization/unification. The *deep* arity [vector] does not have any > boundable length until we determine how any generic return type (i.e. a > return type specified by an as-yet unresolved type variable) resolves. > > As long as the return type is abstract (i.e. a type variable), the > possibility remains that the arity vector (in the way that Keean is writing > it) may grow. as a consequence of unification. > > To the extent that this is true, some of his arity lists are incomplete.
This is a good point. I don't remember any incomplete arity lists though. Rembmer, my list of deep arities was for an example where I assumed the types to be concrete. But none of that seems to address what I'm asking about maximum (shallow) arity. How can we tell that the maximum arity of (fn 'arity Nat->Nat->'a) is 2? How about (fn 'arity Nat->Nat->String->Float)? As an instance of the previous one, it should still be 2. But of course that type could be inferred from some other application in which case the max could also be 1 or 3. If I'm wrong that there's a maximum arity, what prevents (fn 'arity Nat->Nat->'a) from unifying with (fn 3 Nat->Nat->String->Float)? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
