On Wed, Mar 18, 2015 at 9:57 AM, Jonathan S. Shapiro <[email protected]> wrote:
> On Sat, Mar 14, 2015 at 3:53 PM, Matt Oliveri <[email protected]> wrote:
>>
>> On Sat, Mar 14, 2015 at 1:23 PM, Jonathan S. Shapiro <[email protected]>
>> wrote:
>> > I can't write this using your notation, because the afn notation doesn't
>> > say
>> > what I need. I think the *correct* substitution of an abstract function
>> > type here would be to substitute
>> >
>> > 'a -a1-> 'b -a2-> 'c => 'r
>> >
>> > for the 'a parameter type in my typing of choose_one. By unmasking the
>> > effect variables, it becomes clear that all of the arities have to go in
>> > positionally correlated ways.
>>
>> Well I suppose that would take care of it, but are those really
>> effects? It seems like it's really just answering "Function type
>> really here? y/n" Saying between which argument types there is a cfn
>> is _exactly_ what an afn's deep arity does.
>
> So no, I agree, these aren't really effects, or at least they don't behave
> the same. They are effect-like in the sense that there is a property bound
> to the arrow that we need to deal with in the checker. In a much weaker
> sense, they are effect-like in the sense that if your checker or inference
> engine already needs to deal with effects then there is a natural place in
> the implementation to deal with this as well.
>
> I've been trying to pin down what the difference actually is, though. In
> essence, I think it's the fact that we aren't dealing with a subtype
> relation.
>
> So (e.g.) if we had three functions nh1 ha2 nh3 (nh: no heap, ha: heap
> allocating), we would generally say that
>
> choose_one nh1 ha2 nh3
>
> is a legal call. The three types meet on the return type in the usual way
> for subtypes, using an inequality constraint, with the result that the
> return type is *potentially* allocating. The thing about inequality
> constraints is that they are only weakly bidirectional; unless we get some
> further constraint on the return type, no change will back-propagate into
> the types of nh1, ha2, nh3. Or rather, an inequality constraint propagates,
> but is immediately statisfied by the pre-existing "allocation types".
>
> By contrast, the "this arrow is really a call arrow" is not a subtyping
> issue. Either the call happens, or it doesn't. It's an equality constraint
> rather than an inequality constraint.
This is a good point. I just meant that semantically, a callvar
doesn't seem to be about effects since there may not even be a
function call to have effects in the first place.
I don't know the details of effect inference, so I can't say much
about how callvar inference would/wouldn't combine with it. But
something to keep in mind is the type constraint style of arity
abstraction, where the constraints are inequality constraints in the
Keean order--essentially a partial order on deep arities, lifted to
deal with the curried cfns. The order on effects might turn out to
combine gracefully with the Keean order.
>> I've attached a short table showing how your (mixed arrow with
>> "effect" variables) type above does the same thing as (afn 'ar 'a 'b
>> 'c=>'r).
>
> I looked at your table. It appears to me that we are encoding the same
> things in different ways, and that either will work. It also looks to me
> like we share a common awkwardness in our encodings.
>
> 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.
> 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.
> In any case:
>
> Unless there is a reason to prefer the afn notation that I may not be
> seeing, I think I would prefer to pursue this using the effect-like variable
> approach. I don't think it's a better (or worse) encoding, but I think that
> writing type rules in the callvar style may be clearer (if only to me). Is
> there something else here that I may be missing?
There seems to be a strangeness to the mixed arrow/callvar approach
that doesn't come up with afns.
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. So what
does (int->int) mean? How can that arrow turn out to be anything other
than "=>"? Worse, what does ('a->'a) mean? What if it's actually
(int->int) but we don't know it yet, and we say the arrow is not a
call arrow? It seems to me that we really can't do anything until we
have a call arrow to work up to. And there will practically always be
one, since an application must involve at least one call, so we infer
a call arrow (and zero or more abstract arrows) from an application.
With afns, there's effectively a built-in call arrow after the
arguments grouped into an individual afn, so (int->int) and ('a->'a)
are actually inexpressible, which seems right.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
