On Sun, Mar 1, 2015 at 11:35 AM, Jonathan S. Shapiro <[email protected]> wrote:
> On Sat, Feb 28, 2015 at 8:19 PM, Matt Oliveri <[email protected]> wrote:
>>
>> Let me know if you can nest arity-abstract function types. Like:
>> fn 'ar1 'a->'b->'c->(fn 'ar2 'd->'e->'f)
>
> I am not sure how to answer this, because in one sense the answer is "yes"
> and in another sense the answer is "no".
Uh oh. That was supposed to be a pretty concrete question. It's
amazing, in a bad way, how two people can look at the same incomplete
explanation and invent entirely different details to fill the gaps.
> Let's ignore arity for just a moment in order to ask this question more
> generally: if we are working with HM-style function types, can you nest
> *those* in the way that you ask? That is: is there any difference between
>
> fn 'a->'b->'c->'d->'e->'r
>
> and
>
> fn 'a->'b->'c->(fn 'd->'e->'r)
>
> I think the answer to this is obviously "no". Or alternatively, the answer
> to this is obviously "yes", and we should understand
>
> fn 'a->'b->'c->'d->'e->'r
>
> as a shorthand for:
>
> fn 'a->(fn 'b->(fn 'c->(fn 'd->(fn 'e->'r))))
I think the answer is that "fn 'a->'b->'c->'d->'e->'r" is a syntax
error. HM function types always take one argument.
> that is: the conventional arity notation is a convenience shorthand for the
> fully nested one. The only sense I can see in which this is *not* a good
> interpretation is that we don't know whether 'r will end up unifying with a
> function type, and our nesting may get deeper as a result. That seems a
> little odd for a convenience shorthand, but certainly not impossible. Merely
> odd.
What is the "conventional arity notation"?
Is that "fn 'a->'b->'c->'d->'e->'r"?
Or "fn 'arity 'a->'b->'c->'d->'e->'r"?
Or something else?
There's definitely something odd about saying "fn
'a->'b->'c->'d->'e->'r" is short for "fn 'a->(fn 'b->(fn 'c->(fn
'd->(fn 'e->'r))))". I mean the main odd thing is why the first form
even exists, since you're not attaching anything to it that applies to
the entire nested group of function types as a whole. But also, as you
said, because of it possibly not capturing the full curried function
type, because of 'r possibly instantiating to a function type.
In the case where we assign an arity to the group of functions, the
first oddness goes away. The second oddness is still somewhat odd, but
the possible explanation is that we've grouped the functions according
to how they are arity-abstractly applied. That explanation would
suggest that nesting arity-abstract function types is sensible.
> So now getting back to your question...
>
> When I wrote:
>
> ('arity < 5) => fn 'arity 'a->'b->'c->'d->'r
>
> [which, incidentally, should say 'arity > 0 for clarity, thought that is
> subsumed by the fact that the basic arrow type does not admit functions of
> zero arity]
There's no technical problem with leaving out ('arity > 0). That can
be an implicit requirement of the "fn" notation's parameter.
> I said we "knew" (by magic) that 'r would not take on a function type. The
> 'arity here is being written in the same sort of intuition that the arrow
> notation is a convenience shorthand for the fully nested composition. And on
> reflection, it's actually a poor intuition, because in practice 'r *can*
> unify with a function type.
Yes, I agree. It does seem to suggest that this is the "fully nested"
composition of function types. But we know that isn't right. My
alternative intuition explained above is that we've grouped some
"prefix" of the fully nested function type into a special notation to
talk about the abstract arity of the whole prefix. There is no way for
arity to be abstract if we spell out how the arity-concrete function
types are nested.
You might not follow the above because AFAIK you consider (fn 2
'a->'b->'c) to be literally, syntactically the same as (fn 'arity
'a->'b->'c), once you've substituted ('arity := 2) in the latter. I
think it's a mistake to conflate arity-concrete and arity-abstract
function types like that, because they serve different purposes.
How about, for the time being, we use (cfn 2 'a->'b->'c) and (afn
'arity 'a->'b->'c)? Substituting into the afn gets (afn 2 'a->'b->'c),
and I'm not entirely sure I know what that's supposed to mean, because
of the ('ar := 1) vs. ('ar := 1 + 'newArity) issue. On the other hand,
the 2 in the cfn is definitely, non-negotiably a shallow arity.
> So another way to look at this would be to write
> it as:
>
> f :: ('nargs >= 4) => fn 'nargs 'a->'b->'c-'d->'r
Now you're getting weird. From your previous email, I thought the
point of ('arity < 5) is to prevent partial applications. I don't
understand how ('nargs >= 4) prevents this. We don't need to say
anything additional to see that f can be applied to at least 4
arguments, because its arity-abstract type already lists 4 argument
types. We can safely apply more arguments than the native shallow
arity might turn out to be.
> with the intended interpretation that f is some [composition of] functions
> such that f takes at least four arguments, and may take more depending on
> how r unifies. Following the arity-free convenience syntax intuition above,
> this can be viewed as a shorthand for:
>
> f :: fn 1 'a -> fn 1 'b -> fn 1 'c -> fn 1 'd -> 'r
Whoa, I didn't know that. I thought that type was arity-concrete (up
until you get an 'r, which may be an arity-abstract function).
> where 'r is completely free, an in particular may unify with fn 'nargs ...
> for any 'nargs, but simultaneously need not unify with a function type at
> all. And in *that* interpretation of things, we're saying that we are
> permitted [inductively] to combine smaller arities into higher arities and
> rewrite the application AST, such that (inductively)
>
> fn 1 'a -> (fn 1 'b -> 'c)
>
> may be "composed" into
>
> fn 2 'a->'b->'c
So how would you actually write a function type whose native shallow
arity is 2? I'm starting to think I actually have a quite-different
proposal from yours, and that we should start over, explaining our
proposals in more detail.
> which may in turn be combined further. So in this view we are starting with
> all arities equal to 1 (which is the curried view) and coercing the arities
> *upwards* within the type rule for /app/.
>
> This actually might be a more consistent and simpler way to think about
> things.
But what drives specialization? How do you talk about the types of
defined functions, which are arity-concrete, and how they unify with
arity-abstract function types?
> I'm not sure whether this is helping or not, so I want to stop here to give
> you a chance to read and see if you can help refine either the question or
> my answer.
It's helping by uncovering massive differences in our thinking.
> Haven't forgotten the other question, but I think that refining this one may
> possibly lead us to a different answer there, so let's tackle this one
> first.
It seems you want afns to be nestable. But, unlike me, you think afns
can be "groupped" or "ungrouped" between nested afns. And you don't
seem to have cfns in your syntax at all. Yes, we probably should work
this out before (or at the same time as) we worry about how the arity
parameter of an afn is interpreted.
> So: do the intuitions that I have sketched above make sense,
No.
> and if so, do
> you think it's better to "compose up" or "decompose down"?
For me, the grouping of nested afns, assuming it's allowed, reflects
the individual arity-abstract applications. We cannot regroup them
because that would change the requirements on the concrete instances.
Each arity-abstract application, individually, must not specialize to
involve an arity-concrete partial application. In other words, it must
specialize to one or more exactly-matching arity-concrete
applications. You cannot split an arity-concrete application between
two arity-abstract applications.
> I actually think
> this is related to Keean's subtyping view, though at the moment I would not
> want to formalize it that way.
It's quite different, if I'm understanding you both. Keean doesn't use
afns at all. You use afns exclusively. cfns cannot be regrouped freely
because that would denote different native arities. Keean allows
upcasts from "more-curried" nests of cfns to "less-curried" nests,
which is a coercion that doesn't introduce an allocation, as long as
it's inlined into a definition or application.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
