On Wednesday, March 18, 2015, Matt Oliveri <[email protected]> wrote:
> On Wed, Mar 18, 2015 at 9:57 AM, Jonathan S. Shapiro <[email protected] > <javascript:;>> 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. 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. > > 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? I assume whenever a (a->b) type expression appears in mixed arrow, > it's just short for (a-a1->b), where a1 is a fresh callvar. Right. > So what > does (int->int) mean? 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. > How can that arrow turn out to be anything other > than "=>"? It can't. > 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. 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. > 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. 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. Jonathan
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
