On Tue, Mar 31, 2015 at 4:57 PM, Keean Schupke <[email protected]> wrote: > More on choose_one: > > choose_one :: a -> a -> Bool -> a > choose_one x y b = if b then x else y > > f1 :: a => b c => d > f1 x = \y z . x +y + z > > f2 :: a -> b -> c -> d -- I am not sure if this should infer > f2 x = \y . \z . x + y + z > > g = choose_one f1 f2 random_bool > > inferred type of choose_one: > > (a => b c => d) U (e -> f -> g -> h) = (a => b c => d)
That's not the type of choose_one. That's the type choose_one's "a" becomes. The type of choose_one is (a=>b c=>d)->(a=>b c=>d)->Bool->(a=>b c=>d) right? Your f1 and f2's types not a good pair of function types to test it on. Shap pulled this too. If it doesn't stay arity-abstract, you're not testing what I want. How 'bout f1 : a->b->c->d f2 : a->b->c->d ? 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. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
