On Sat, Mar 14, 2015 at 1:23 PM, Jonathan S. Shapiro <[email protected]> wrote:
> On Fri, Mar 13, 2015 at 2:14 PM, Matt Oliveri <[email protected]> wrote:
>> On Fri, Mar 13, 2015 at 11:06 AM, Jonathan S. Shapiro <[email protected]>
>> wrote:
>> > I think it's also interesting to look at apply_one. Reusing f1, f2, f3
>> > from
>> > above, here is apply_one:
>> >
>> > def apply_one x y z a b c {
>> > if random_true_false ()
>> > x a b c
>> > elseif random_true_false()
>> > y a b c
>> > else
>> > z a b c
>> > apply_one:: cfn ('a->'a->'a->'r) ('a->'a->'a->'r) ('a->'a->'a->'r) 'a 'a
>> > 'a
>> > => 'r
>> >
>> > This case is interesting because the three function argument types do
>> > NOT
>> > unify. And *because* they do not unify, the application
>> >
>> > apply_one f1 f2 f3 1 2 3
>> >
>> > type checks (and specializes) correctly, which is what we want.
>>
>> I agree. With afns too, x y, and z would not get unified. So each afn
>> would each have a fresh arity variable inferred for it. Here's an
>> example that's really funny because in HM it'd be functionally
>> equivalent to apply_one, but the function types do unify, and this
>> means that it's not even the same type in BitC.
>>
>> def not_apply_one f1 f2 f3 a b c = (choose_one f1 f2 f3) a b c
>>
>> See there's only one application to specialize. Oh well. The thing
>> that's so funny about this example is that it's also the example that
>> breaks your scheme.
>>
>> Here's the type I'd give it:
>> not_apply_one : cfn (afn 'ar 'a 'b 'c->'r) (afn 'ar 'a 'b 'c->'r) (afn
>> 'ar 'a 'b 'c->'r) 'a 'b 'c -> 'r
>>
>> The three function arguments must have the same arity, as you can see.
>>
>> Here's the type I suppose you'd give it:
>> not_apply_one : cfn ('a->'b->'c=>'r) ('a->'b->'c=>r) ('a->'b->'c=>r)
>> 'a 'b 'c => 'r
>>
>> You (correctly) do not infer an arity-concrete type for f[123], since
>> there is no reason to do so. But what's wrong with that type? Well,
>> AFAICT, the arguments do _not_ need to have the same arity! We can
>> instantiate each one separately, like:
>> cfn (cfn 'a 'b 'c=>'r) (cfn 'a 'b=>cfn 'c=>r) (cfn 'a=>cfn 'b 'c=>r)
>> 'a 'b 'c => 'r
>>
>> Now we use functions of different arities for f1, f2, and f3. Oops.
>
> Let me start with a question. You wrote "AFAICT, the arguments do _not_ need
> to have the same arity!", but I am not clear which function you are
> referring to here. If you are referring to choose_one, then my answer is:
> yes they do, because all of those types meet at the return type.
The first three arguments of not_apply_one. We agree that these
arguments _should_ have the same arity. What's not clear to me is how
your type system _enforces_ that.
> A consequence is that no, I would NOT type not_appply_one in the way you
> suggest. Something went wrong here, and it is the reason I wanted to appeal
> to an effect-like intuition about the arrows.
>
> My originally given type for choose_one was:
>
> cfn 'a 'a 'a => 'a
>
> You went and substituted ('a->'b->'c=> 'r) through for 'a on my behalf,
Something like that. Just to make sure, I'll go through how I got that
type soon.
> which is perfectly good as a term substitution in HM, but it's no good here.
Hmm, well that's for sure. But what's the alternative? Here's how I
got the type:
We apply choose_one to f[123]. Now f[123] have the same type, call it
'f. The type of (choose_one f1 f2 f3) is also 'f. So far a, b, and c
could have arbitrary types, like 'a, 'b, and 'c, respectively.
We apply (choose_one f1 f2 f3) to a, b, and c, with no apparent need
for multiple calls, so we infer that 'f is ('a->'b->'c=>'r), where 'r
is a fresh type variable. ((choose_one f1 f2 f3) a b c) has type 'r,
and that's the result of not_apply_one. So not_apply_one has type (cfn
'f 'f 'f 'a 'b 'c => 'r).
But 'f is ('a->'b->'c=>'r) so not_apply_one has type:
cfn ('a->'b->'c=>'r) ('a->'b->'c=>'r) ('a->'b->'c=>'r) 'a 'b 'c => 'r
So really, the problem with mixed arrow types is very basic: they're
not really types because you can write the "same" one twice, and it
could mean something different each time. I guess this is the same
point as that you can't substitute ('a->'b->'c=>'r) for a type
variable.
> The reason it's no good is that the identity-of-types requirement has been
> lost in the substitution. The reason that happened is that this way of
> writing the type is conceptually incomplete.
I think we're on the same page.
> The reason it is incomplete is
> that you have omitted the effect type variables on the arrows. Once those
> are restored, the necessary identities will once again be preserved.
You didn't say anything about an effect variable, you trickster! :)
> 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.
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).
a -a1-> b -a2-> c => r
vs.
afn ar a b c => r
This table shows how mixed arrow and afn notation for arity-abstract types
would express the same curried cfns, for concrete values of the appropriate
variables.
a1 a2 | ar | cfn
------+---------+-----------------------
n n | [3] | cfn a b c=>r
y n | [1,2] | cfn a=>cfn b c=>r
n y | [2,1] | cfn a b=>cfn c=>r
y y | [1,1,1] | cfn a=>cfn b=>cfn c=>r
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
