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. Keean. 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 > _______________________________________________ > 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
