On Mon, Mar 30, 2015 at 1:14 AM, Jonathan S. Shapiro <[email protected]> wrote:
> On Fri, Mar 27, 2015 at 7:37 PM, Matt Oliveri <[email protected]> wrote:
>> On Fri, Mar 27, 2015 at 10:48 AM, Jonathan S. Shapiro <[email protected]>
>> wrote:
>> > OK. On to Matt's concern. In essence, it seems to be that we have two
>> > parameters that cannot specialize independently. So when we see:
>> >
>> > 'a->...->'b-?r->'c
>> >
>> > we can specialize that '?r' to 'y' only if we know that 'c is not a
>> > function
>> > type (which therefore might introduce more arrows on the right).
>>
>> That's not what I was saying. It's that we can only specialize ?r to n
>> if we know that 'c _is_ a function type. I don't think there'd be any
>> situation where we can't specialize to y.
>
>
> Thanks for saying it again.
>
> So I agree that in principle this is awkward, but I'm not convinced that it
> arises in practice.
>
> First, the only inference scenario where we might be tempted to infer
> something like 'a->'b->'c is in the context of an application like
>
> f a b
>
> but in that context the correctly inferred type would be 'a -?-> 'b -y-> 'c.
Right, this is what I've been saying. You always have a call arrow, so
afns are sufficient.
> More generally: in the scheme that I have been outlining it is intentionally
> true that specializations from ?r to 'y' occur through a different mechanism
> than specializations from ?r to 'n'. Basically: applications can cause a
> specialization from ?r to 'y', and specializations to cfns can induce
> specializations from ?r to 'n'. In the ?r to 'y' case, as you note, the
> specialization can always be safely be performed (though it may result in a
> later type incompatibility). In the ?r to 'n' case, the fact that this
> specialization can only arise from specialization via a cfn means (because
> cfns always have an explicit return arrow) that the specialization can only
> occur in contexts where doing so is correct.
>
> This is exactly why I originally described arrows as having only the ?r and
> 'y' options, and not the 'n' option. Eliminating the 'n' from the arrow type
> syntax means that it's impossible to introduce an incorrect arrow type even
> by hand. Allowing them to be specialized by cfns INTO cfns has the effect
> that n-ary calls get introduced in a structured way, without the risk of 'n'
> appearing in the wrong place.
Ah. Yes, I think you're right. Another way to say this is that by not
allowing the user to write 'n' arrows, and only instantiating due to
unification, all types that ever arise could've been expressed as
afns. So the system will be sound if the afn version is. It's a sneaky
argument.
>> > Aside from the fact that I've probably boogered the
>> > writing of the rule somehow, the real problem is that it isn't really
>> > syntax driven.
>> > It's very much like an implicit coercion that way.
>>
>> I don't know what you mean. What's "syntax driven"? Is that the same
>> as syntax-directed?
>
> Yes. I probably should have written syntax-directed. It matters because this
> rule (as I have written it) doesn't get applied according to the inductive
> structure imposed by constructions. It inadvertently introduces bounded but
> nondeterministic search into the type inference process, which isn't a good
> thing.
OK that makes sense.
> I think the right thing to do for now is to write using AFN, and then we can
> go back later and figure out if a notation more similar to ML and Haskell
> conventions is pragmatically tolerable.
>
> In order to discriminate your afns from mine in our discussion, I propose
> that you write the arity type variable as ?r rather than 'r.
But, to be clear, the ?r is a deep arity variable?
>> > The problem that
>> > this rule introduces is a problem of convergence; we need to confirm
>> > that if
>> > two type rules modify this arrow, they do so with the same result.
>>
>> So you mean we need to be sure that the same type doesn't get
>> instantiated in incompatible ways in different places? But I figure
>> what you're saying with that rule is that we can only instantiate the
>> callvar a certain way once we know enough about the return type. So
>> how would that happen?
>
> I don't think that it *is* possible. But if we are looking at
>
> 'a -?r->('b :: non-function)
>
> its possible that we can unify something (on the one hand) or apply the
> arrow promotion (on the other). At that point we have a divergent search
> happening, and it's important that all paths through the rewriting graph end
> up with the same answer.
I don't understand. But it seems like neither of us like the rule, so
never mind I guess.
>> > I provisionally think that the problem of non-independent type variables
>> > applies to afn types as well. When I specialize the argument type
>> > variables,
>> > I have to update the arity type variable as well. Perhaps Matt can
>> > explain to me why that isn't an issue?
>>
>> I don't see why type variables in the argument types would affect
>> anything. I am not trying to make tuplized arguments and multiple
>> arguments look the same, if that's what you're thinking. (That might
>> not be a bad idea, but I haven't been thinking about it at all.)
>>
>> Can you give an example where an argument type affects the arity of a
>> function in any way?
>
> I'm not sure, but let me try.
>
> The difference between an AFN and a CFN is that the AFN does not say *how*
> the arguments must be consumed. So in particular, it's reasonable to rewrite
> (through unification)
>
> afn ?r 'a 'b -> 'c
>
>
> with
>
> afn ?r1 'a -> afn ?r2 'b -> 'c
>
>
> in which the arities have degenerated to '1' because each afn accepts just
> one argument and the arity is therefore known. The point here is that the
> rewrite has to update a bunch of variables in a consistent way rather than
> updating just one at a time.
I don't see any type variables changing in this example. We still have
the same type variables 'a, 'b, and 'c. What did happen is ?r was
instantiated to (?r1 ++ ?r2), where "++" is list append. Maybe this is
all you mean by dependency between type variables. It doesn't bother
me since instantiation is constrained only by syntactically-available
information.
I guess it's time to explain why (afn (?r1 ++ ?r2) 'a 'b -> 'c) and
(afn ?r1 'a -> afn ?r2 'b -> 'c) are the same type. I think of "afn"
as a type-level computation which ultimately reduces to some type
formed with cfns. While the arity remains abstract, we cannot do the
reduction, so we don't know what the cfns are, but because afn is
"just" a total function producing a type, it must mean something.
The afn function takes a deep arity (with some obvious constraints), a
list of argument types and a return type. So (afn ?r 'a 'b -> 'c) is
sugar for something like (rawAFN r [a,b] c), where "rawAFN" is the
actual function. It's defined recursively:
rawAFN [] args rtn = rtn // That weird base case
rawAFN (a :: r) args rtn = rawCFN (firstn a args) (rawAFN r (skipn a args) rtn)
Oh yeah, rawCFN takes a list of argument types and a return type.
The constraints on the deep arity argument of rawAFN are:
- Each element is an integer > 0.
- The sum of the elements is the length of the list of argument types.
So in the case of (afn ?r1 'a -> afn ?r2 'b -> 'c), for the type to be
well-formed, ?r1 sums to 1, and so does ?r2. That means that (?r1 ++
?r2) sums to 2, so (afn (?r1 ++ ?r2) 'a 'b -> 'c) is well-formed. (So
we can instantiate ?r to (?r1 ++ ?r2).) And in fact you can prove from
the recursive definition that the two types are equal, by induction on
?r1. (I'm pretty sure.)
Of course in this case ?r1 and ?r2 must be [1], but I tried to give
the general argument for why we can split an afn. (Splitting an afn is
analogous to instantiating a callvar with 'y'.)
Clarification: "rawAFN" and "rawCFN" would not be valid BitC syntax.
They are in some make-believe metalanguage in which we might embed the
BitC type system. In particular, the argument lists in BitC syntax
cannot be abstract, so we can count the elements. I'm not sure yet if
we'll actually ever need to write "++" or "::" for arity lists either.
Mixed arrow notation suggests that we will not.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
