On Thu, Mar 19, 2015 at 4:44 PM, Jonathan S. Shapiro <[email protected]> wrote:
> On Wednesday, March 18, 2015, Matt Oliveri <[email protected]> wrote:
>> On Wed, Mar 18, 2015 at 9:57 AM, Jonathan S. Shapiro <[email protected]>
>> wrote:
>> > There are actually three "values" that the variable on an arrow can take
>> > on
>> > (I'll call this variable a "callvar" below)
>> >
>> > not-yet-bound
>> > is-a-return-point
>> > not-a-return-point
>>
>> What do these mean? Especially the first.
>
> I should have written "free" for the first one. I meant a type variable that
> hasn't yet been specialized.
Oh, well it's not a value then, it's a variable. :) So it sounds like
there are two possible values, as I figured.
> The second one is the double arrow =>
>
> The third one we haven't yet assigned a symbol to. It's the one that
> disappears when a cfn having arity>1 is used and we end up with n arguments
> that replace n-1 non-call arrows. That's what I mean (just below) when I
> talk about cfn fixing these, though it doesn't so much fix them as replace
> them with multiple arguments.
I agree. These were the "y" and "n" in my table.
>> > In my case, the discussion where I introduced the => arrow was talking
>> > about
>> > abstract arrow types, In such types, the is-not-a-return-point case
>> > doesn't
>> > arise, because we haven't introduced concrete arities yet. In *both* of
>> > our
>> > notations (I think), the consequence of writing "cfn" is that it fixes
>> > any remaining unbound callvar to not-a-return-point.
>>
>> I'm afraid I don't know what you're talking about.
>
> Any clearer now?
So in other words, we haven't had to write down any "n" arrows, but,
for example,
cfn 'a 'b 'c=>'r
and
'a-n->'b-n->c-y->'r
are the same type.
> It should be read initially as int-a->int, where a is a fresh type variable.
> But it immediately reduces to int=>int, essentially because you can't have
> zero arguments and the type on the right of the arrow is known to be a
> non-function type.
OK I guess.
>> Worse, what does ('a->'a) mean?
>
> This is harder, but I think it may be better to discuss 'a->'b, because the
> problem is entirely on the right of the arrow. We should read it initially
> as
>
> 'a-'a1->'b
>
> Where 'a1 is a fresh type variable. We cannot reduce -'a1-> to =>, though,
> because we do not know yet whether the 'b may specialize to an arrow type
> having a further callvar. We therefore don't have enough information here to
> conclude that this just be a single argument function.
Semantically, I completely agree. But you're saying we have a variable
we're not allowed to instantiate. That's what I'm saying is weird.
> Part of the confusion here is purely visual. Arrows do not visually suggest
> nesting, but nesting is what they actually do. In this case we have
> something unresolved in the innermost part of the nesting structure.
But the callvar is not part of the unknown return type, yet we cannot
safely instantiate it independently from the return type. This is,
more specifically, what I'm saying is weird.
>> What if it's actually
>> (int->int) but we don't know it yet, and we say the arrow is not a
>> call arrow?
>
> As long as the type variable on the right of the arrow remains unresolved,
> we cannot fix the arrow type unless we do so as a consequence of unification
> with something else that forces a resolution.
Yeah, that's weird. There are all these ways of explaining the needed
restriction, which I think is weird. But the reason it's weird is that
it seems to mean we can't think of variables in types as being bound
by implicit quantifiers anymore, because instantiation of quantifiers
would not be able to express this restriction.
> I agree with you that afns always have a call arrow, but much of the point
> of the current discussion is that we don't know where the intermediate call
> arrows may be.
The call arrow built into an afn isn't an intermediate one though,
it's the last one. Every application has a last call, no matter how it
specializes. I'm saying afns can express all the arity-abstract types
we need, but doesn't require special restrictions on when variables
can be instantiated, because it doesn't express ('a-'a1->'b), which is
not needed. This is why I still prefer afns to mixed arrow.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
