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
