On Sat, Feb 28, 2015 at 10:15 PM, Jonathan S. Shapiro <[email protected]> wrote:
> On Sat, Feb 28, 2015 at 5:25 PM, Matt Oliveri <[email protected]> wrote:
>>
>> > 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.
>
> So just to confirm, I *think* this means the maximal concrete arity that
> might legally specialize a given abstract arity?
Not quite. I don't think of maximum shallow arity as a property of an
abstract arity, but of an arity-abstract type.
>> 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.
>
> Oh. Oh! No, I do not believe this is correct. Or at least I think there may
> be a better way to think about it, and I also think that (if I am
> understanding your term correctly) "maximum shallow arity" isn't sufficient.
I'm now pretty sure you're right that maximum shallow arity isn't
sufficient. I may have made a bad assumption that arity-abstract
function types don't get nested. The solution seems cleaner if you
nest one arity-abstract function type per arity-abstract application.
The thing that confused me is that ideally, we'd coalesce consecutive
arity-abstract applications into one. But we can't do that across
modules, and it may be too messy to demand it even within modules,
since it affects type inference.
If you're using one arity-abstract function type per arity-abstract
application (which seems obvious in hindsight), then it seems very
plausible that you are handling this issue successfully. But I can't
be sure until I understand what's going on with unification in your
scheme.
> I think that a better way to think about this is to imagine that an abstract
> arity is accompanied by a constraint. Thus, if we see an application for
> unknown function f taking the form
>
> f a b c d
>
>
> we should not merely infer
>
> fn 'arity 'a->'b->'c->'d->'r
>
>
> We should instead infer
>
> ('arity < 5) => fn 'arity 'a->'b->'c->'d->'r
I saw you use this notation before, but you've said so little about
it, I wasn't sure it would be inferred. Good. Now if only I knew what
kind of arity 'arity is. (Yes, I know it's a nonzero Nat.) It's still
ambiguous whether it's a total arity or a shallow arity. Admittedly,
"total arity" is a confusing name if you allow nested arity-abstract
functions.
> And I think that we *can* apply a concrete function f_c having (say)
> concrete arity 2, provided the overall type signatures unify. Allocation may
> or may not happen in this case. It depends on whether f_c returns a
> newly-formed closure or not. But the point is: if it returns a closure then
> the allocation happened within the body of f_c as an operation explicitly
> stated by the programmer, and that's okay.
Right.
> Meanwhile, thank you for clarifying the rest of those definitions.
Let me know if you can nest arity-abstract function types. Like:
fn 'ar1 'a->'b->'c->(fn 'ar2 'd->'e->'f)
I'll need to tweak my definition of deep arity if you allow this. It
would no longer make sense to unambiguously assign a single deep arity
to a concrete type. Intuitively, deep arity is assigned relative to a
given return type whose arity is locally considered to be nil.
Alternatively, you could leave "deep arity" alone, but then it's not
what I'm proposing to use anymore, since that definition was an
accident of my no-nest assumption.
I'm also looking forward to a reply where you resolve my confusion
about ('ar := 1) vs. ('ar := 1 + 'newArity).
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
