Hmm but that variable does not follow normal unification rules. Its not a type variable, but looks like a kind of expansion variable?
We agree that arity-aware types break paretricity right? K. Keean. On 1 Apr 2015 08:03, "Matt Oliveri" <[email protected]> wrote: > 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 >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
