On Thu, Mar 19, 2015 at 3:11 PM, Matt Oliveri <[email protected]> wrote:
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.
>
I think so, yes.
> >> 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.
>
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.
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.
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?
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.
>
> >> 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).
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
