On Fri, Mar 20, 2015 at 1:10 PM, Jonathan S. Shapiro <[email protected]> wrote:
...
>> > 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.
>
> I agree it's weird, but that's not *quite* what I'm saying. I see the point
> you are making, and I agree with it. My qualifier is that there are *other*
> things that can cause it to be instantiated. E.g. if
>
> a-?->b
> c=>b
>
> unify for some reason, then it's okay to fix the variable. More generally,
> it's okay to fix the variable to "does-return", without knowing the return
> type, but not necessarily okay to fix the variable to "does-not-return".
> Which makes sense, because that arrow might, in fact, return.
Right, basically we would need some restrictions to prevent ('a-n->B)
from arising, where B is a concrete, non-function type. Because that
type is nonsense. To me this is a symptom of bad type syntax.
> But another way to look at it might be that 'a -n-> 'b tells us that 'b
> *must* be a [multi-]arrow type that eventually includes a constituent =>
> arrow somewhere. That is: the existence of a -n-> arrow is effectively a
> constraint requiring that some return must occur somewhere to the right of
> that same arrow.
I suppose that perspective is workable, but I really don't like it.
What's so bad about afns, which avoid this issue entirely, that you'd
rather invent a new kind of constraint?
>> 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.
>
> I agree that this is weird. There is something constraint-like going on
> here. What we're really saying is that once you see a -n-> arrow, the free
> type variables to the right of that are no longer free to unify arbitrarily.
> Similarly, we are saying that if the type in tail position is NOT a function
> type, then the -?-> arrow just before the tail position must be a => arrow.
> Which makes common sense, given that functions must return.
>
> So this raises two questions:
>
> 1. How to record this in a vaguely coherent type system.
> 2. Is it in fact the case that functions must return?
You seemed to have missed the point that this problem of mixed arrow
notation is entirely an artifact of the notation. There is no semantic
problem to solve here; applications always involve at least one
function call, and notation that ostensibly allows "functions" that
can be applied with no calls is not a good fit for the situation.
I know you're trying to figure out how to ensure you don't actually
get a function type with no calls, but you're trying to fix a problem
that you created with your notation!
So:
1. Express function types using afns, or something similar, where a
call arrow must always be syntactically present.
2. You may be taking "does-return" and "does-not-return" too
literally. A function type usually doesn't tell you anything about
whether the function returns.
> What I'm leading up to in the second question is the possibility of
> co-routines or [a]synchronous send. But my feeling is that those should be
> modeled as returning unit.
Function types in most programming languages are partial function
types. They tell you the type of value a function will return, if it
in fact does return. It may not. You can guarantee a function will
_not_ return by giving it a return type of bottom, or (sometimes) a
type variable that doesn't appear anywhere else.
The y and n values of a callvar really have nothing to do with that.
You can't even _call_ an element of ('a-n->'b) because we haven't
assembled its concrete arity yet. ('a-n->'b) is kind of a fake type,
since you can't introduce or eliminate it. In contrast, with the
afn/cfn system, afns are applied, and cfns are called. (Nice how the
initials match up.)
>> >> 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.
>
> But I think we can rescue most of that if we can introduce a suitably
> predicated qualifier (i.e. constraint).
Probably, but please first explain why you don't want to use afns.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
