Sorry, I realized the connection between nested arity-abstract function types and "grouping" was not made clear in the previous message.
On Tue, Mar 10, 2015 at 8:26 AM, Matt Oliveri <[email protected]> wrote: > On Tue, Mar 10, 2015 at 1:45 AM, Jonathan S. Shapiro <[email protected]> wrote: >> The other thing I've been thinking about is this question of arity-as-list. >> Going back to the example above, >> >> f a b c >> >> has several possible realizations as function calls: >> >> f [a] [b] [c] >> f [a b] [c] >> f [a] [b c] >> f [a b c] >> >> So I'd propose as a base case that when a function does NOT return a >> function-valued return value, then it's arity should be expressed as a >> single-valued list. E.g. >> >> def g x y = 1 // arity [2] >> >> if a function g returns a value of concrete function type /cft/, then the >> arity list for g amounts to >> >> nargs(g) :: arity-of(cft) // where :: is, in effect, "cons". >> >> The principal that we concatenate nargs(g) with the arity of g's return >> value, and treat a non-function-valued return value as the empty list, seems >> to hold up pretty well here. In >> >> def g x y = x >> >> the arity list for g is >> >> nargs(g) :: arity-of(x) >> >> >> There may be a cleaner way to think about this, but I provisionally believe >> that we can treat arity-of() as a type-level accessor that returns list(Nat) >> for concrete functions and is treated similarly to an unresolved type >> variable for abstract function types. > > This definition makes sense to me, and matches how I explained deep > arity at first. But I later decided it might not be so useful to > really have deep arity go all the way down to a known non-function > type. It seems more useful to be able to talk about "deep" arity > relative to any chosen return type, which may be a type variable, and > thus, possibly a function type. > > The reason is that what I wanted deep arity for is to distinguish > different arity instantiations of an arity-abstract function type, but > if arity-abstract function types can be nested, then we expect the > return type to sometimes be a function type, and deep arity is about > the arguments before we get to that function type. That is, the > arguments handled by the outer arity-abstract function type. In other words, we use deep arity to describe a group of concrete function types. The arity-abstract function type lets you talk about the group without knowing its deep arity (its composition from individual cfts). Nested arity-abstract function types entails that we've broken up the whole eventual function type into groups, and we concretize the arity group-wise. This helps ensure we don't allow a too-large shallow arity for the way it gets applied, like in the apply[12] example below. >> 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 > > 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 > (That doesn't seem to alleviate the need for grouping though.) _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
