On Wed, Apr 1, 2015 at 2:43 AM, Keean Schupke <[email protected]> wrote:
> On 1 April 2015 at 07:18, Matt Oliveri <[email protected]> wrote:
>> On Wed, Apr 1, 2015 at 2:00 AM, Matt Oliveri <[email protected]> wrote:
>> > Looks easy right? Then choose_one's type becomes
>> > (a->b->c->d)->(a->b->c->d)->Bool->(a->b->c->d)
>> >
>> > But this unifies with
>> > (a=>b->c->d)->(a b=>c->d)->Bool->(a b c=>d)
>> > right?
>> >
>> > Of course it's obviously unsound to use that type for choose_one.
>>
>> It just occurred to me that this issue really has nothing to do with
>> choose_one-like code. We can use the identity function:
>> id : 'a->'a
>> instantiate:
>> id : ('b->'c->'d)->'b->'c->'d
>> unifies with:
>> ('b=>'c->'d)->'b 'c=>'d
>
> Yes, I was in the middle of typing a long reply, that I can now make shorter
> :-)
>
> Its a problem with unification, and you cannot fix it without changing the
> unification algorithm. It does not matter what types you allow to be
> substituted.
>
> Unfortunately the answer appears to be that arity breaks parametricity, and
> so you need to adopt something like intersection types and expansion
> variables (which lead to undecidable unification) to fix it. I hope I'm
> wrong about this.
I'm not sure what you're saying, but it sounds wrong. The solution
isn't so drastic; you just need a variable to ensure that things that
look the same really are the same.
If ('b->'c->'d) is sugar for (afn ?ar 'b 'c->'d), then when we
instantiate ('a->'a) we get
(afn ?ar 'b 'c->'d)->afn ?ar 'b 'c->'d
This doesn't unify with
('b=>'c->'d)->'b 'c=>'d
because that would be trying to make ?ar into two different things.
If we just write
('b->'c->'d)->'b->'c->'d
that's sugar for
(afn ?a1 'b 'c->d)->afn ?a2 'b 'c->'d
which is simply the wrong type, and is not an instance of ('a->'a).
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
