On Fri, Feb 27, 2015 at 2:24 PM, Jonathan S. Shapiro <[email protected]> wrote:
> On Thu, Feb 26, 2015 at 9:58 AM, Matt Oliveri <[email protected]> wrote:
>>
>> ....it looks like you mean maximum total arity, which
>> is indeed unknown in that example. But I really am talking about
>> maximum _shallow_ arity, which is not the same.
>
> Hmm. Through this whole discussion, I have been interpreting "shallow arity"
> to mean the native concrete arity of the leftmost application. That is
> always a simple (singleton) arity rather than an arity vector.

Yes. That's what I mean too. Where by leftmost application, we mean
leftmost application of an arity-concrete function type. (As opposed
to the multiple arity-concrete applications an arity-abstract
application can specialize to.) But another one of your emails makes
me suspect that you're not actually being consistent about this, and
that you're referring to other scalar arity Nats as a shallow arities.

> I'm not sure
> what is meant by the *maximum* shallow arity, so I'm not yet able to use
> that term in a way that is consistent with you.

Very simply, it's the maximum shallow arity that instances of a given
arity-abstract type can have. Even more unambiguously: Take the set of
all concrete instances, take the shallow arity of each, and take the
maximum.

The reason why it's important that we know this is because we cannot
apply with fewer arguments than this, or else an instance whose
shallow arity is the maximum will come along, and our application
would specialize to a partial application, which allocates. So yeah
it's confusing that the maximum arity is the minimum number of actual
arguments. It can't be helped. I think this is how you got confused
over max/min with Geoffrey. (Or was it William?) Going in the other
direction, from an (arity-abstract) application with n arguments, we
infer a type whose maximum shallow arity is n, thus constraining
unification to prevent passing functions that take too many native
parameters.

So to recap, the problem here is that it seems we need to know the
maximum shallow arity, but it's ambiguous from your notation for
arity-abstract types.

Come to think of it, maximum shallow arity may not be enough.

> Aside: I'm disconcerted by using "shallow" and "deep" here, which are
> generally associated with object graphs and pointer traversal. Perhaps I'm
> just not seeing the connection.
>
> So: can you define terms?

Shallow arity: Arity of an arity-concrete function type/definition/application

Deep arity:
The point of deep arity is to formally negotiate the difference
between the formal idea that an actual application provides one or
more arguments simultaneously, and the informal idea of a curried
application which provides zero or more arguments across zero or more
actual applications.

The way I think about arity specialization proposals for BitC is that
the actual applications are arity-concrete applications.
Arity-abstract applications specialize to one or more arity-concrete
applications, adapting to how "natively-curried" the function to apply
is.

There are potentially many arity-concrete function types involved in
an instance of a single arity-abstract function type, one as the
return type of another, as you know. Deep arities reflect this
straightforwardly. I just chose "shallow" and "deep" because the
arity-concrete function types are nested, and "shallow" pertains to
one layer while "deep" pertains to them all.

Formally, the base case is kind of weird. Any non-function type has a
deep arity of nil. (We could technically allow any type to be
considered to have a deep arity of nil, but this allows nested
arity-abstract function types, which is silly, shouldn't arise in
inferred types, and would require a more precise explanation of the
arity-abstract function type notation.) An arity-concrete function
type with shallow arity n that returns a type with deep arity ar has a
deep arity of (n :: ar). (That's a list cons.)

In this manner, all concrete types are assigned a deep arity saying
how we apply them. Or that we don't, if the deep arity is nil.

Total arity: Sum of the elements (shallow arities) of a deep arity. In
other words, the total number of arguments we can apply before we get
a non-function.

>> >> What are some of your favorite concrete types?
>> >
>> > Well, Sakrete is good for a lot of things...   (http://www.sakrete.com)
>
> I can't believe you passed up the chance to play with Sakrete. It's really
> fun stuff! :-)

I considered raising an eyebrow at your pun, but I postponed it until now.
o_O
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to