On Fri, Feb 20, 2015 at 10:34 AM, Jonathan S. Shapiro <[email protected]> wrote:
> On Thu, Feb 19, 2015 at 11:16 PM, Matt Oliveri <[email protected]> wrote:
>
>>
>> So if we start with
>> fn arity a->b->c->d->r
>>
>> and we want call it with two arguments, you say we get
>> fn 2 a->b->c->d->r
>>
>> ...There's still a choice of native arity to be
>> made. So I propose it should really be written:
>> fn a b -> fn newarity c->d->r
>
>
> Yes. Sorry. That's correct, and with the arity variable made explicit that
> is how it should be written.

Well, I don't understand. If (fn 2 a->b->c->d->r) isn't really right,
then the notation isn't really right already with a constant arity.
Making the arity a variable cannot help, right? I was trying to
illustrate something weird by trying to use the arity variable
notation, but really I don't understand it.

It looks like you understand my alternative, and think they both work,
though, so whatever.

If you haven't already, can you look over my explanations to Keean of
arity specialization, and make sure I'm not confused about the
proposal?

========

My other question has to do with the decision that function
definitions always have a concrete arity. Keean seems very interested
in doing something dual, where applications have a concrete arity, and
definitions are specialized to work for their applications. There is
also the a-priori possibility of combining them, using some other kind
of rule to pick the concrete arity. But do these alternatives actually
work?

The original reason I was suspicious of definitions always being
concrete was an example that looked kind of funny that way:

passArith f = f (\x y -> x + y) (\x y -> x - y)
passArith : fn ((fn Nat Nat -> Nat)->(fn Nat Nat -> Nat)->Nat) -> Nat

So this function has a concrete arity, its parameter is
arity-abstract, and its parameter's parameters have a concrete arity.
This seemed weird. However, it seems to work:

useArith plus minus = minus 10 (plus 4 3)
useArith : fn (Nat->Nat->'a) (Nat->'a->'b) -> 'b

useArith' plus = lambda minus = minus 10 (plus 4 3)
useArith' : fn (Nat->Nat->'a) -> fn (Nat->'a->'b) -> 'b

These functions have alternative concrete arities, and their
parameters are all arity-abstract. I picked them because, ignoring
native arity, they can be passed to passArith. And indeed, they _can_
be passed to passArith; all the abstract arities work out. The
useAriths are specialized with 2-applications, and we get passArith
specializations for both useArith arities.

Since your scheme worked better than I expected here, I figure you
should be the one to explain the reason for concrete definitions, and
perhaps reasons against other schemes.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to