On Wed, Feb 18, 2015 at 1:05 PM, Jonathan S. Shapiro <[email protected]> wrote:
> On Tue, Feb 17, 2015 at 9:52 PM, William ML Leslie
> <[email protected]> wrote:
>> choose_one returns one of its arguments; and perhaps x has a curried
>> definition and y takes two arguments directly.  They have the same type, of
>> course, so this is a perfectly reasonable thing to do.
>
>
> This is incorrect, because that is *not* a reasonable thing to do. They have
> the same type. Therefore they are required to have the same concrete type,
> therefore the same arity.

Hopefully you are not saying that whenever the same arity-abstract
type appears twice, the corresponding arity-concrete types are
arbitrarily required to be the same. With choose_one, the native
arities must be the same, but that's because of how choose_one is
defined. I'm about to ask how the type system records this...

>>   But then what instructions do I emit to call f?  It may need to be
>> called twice or once, how do we tell?
>>
>> The only reasonable answer is that choose_one makes a choice of arity for
>> you.  But I can't figure out by your rules which arity it will choose.
>
>
> Either x, y, and z will specialize to the same concrete arity, or the
> expression will fail to type check.

So in order to enforce this, the type of choose_one needs to say that
x and y must have the same native arity, which doesn't follow from
them having the same arity-abstract type. I'm guessing what you meant
to say is that an arity-abstract type is actually a constraint on an
implicitly-quantified arity-concrete type.

In general, writing an arity-abstract type twice will infer a
quantified variable for each of them. But in cases like choose_one,
from the definition of the function, you infer that there's a single
quantified variable. That is what expresses the requirement that x and
y have the same native arity.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to