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".
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))))
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.
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]
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. So another way to look at this would be to
write it as:
f :: ('nargs >= 4) => fn 'nargs 'a->'b->'c-'d->'r
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
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
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.
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.
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.
So: do the intuitions that I have sketched above make sense, and if so, do
you think it's better to "compose up" or "decompose down"? I actually think
this is related to Keean's subtyping view, though at the moment I would not
want to formalize it that way.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
