On Sat, Feb 21, 2015 at 7:22 AM, Keean Schupke <[email protected]> wrote: > let f = choose_one x y z -- different arities > in f n m > > So this code fragment gets the type: > {choose_one :: 'a 'b 'c -> (fn 'd 'e -> 'f), x :: 'a, y :: 'b, z :: 'c, n: > 'd, m: 'e} -> 'f > > Note, you can't type this fragment in HM as it has open types, but we can > type it with named implicit variables as above. > > To know what happens we need a type for choose_one. Whichever of x y z it > chooses will get the type: > > {x :: fn 'd 'e -> 'f ... } -> 'f > > And we can pass any definition into 'x' that satisfies the normal subtyping > subsumption rule.
I don't know how to read most of that, but I think you misunderstood the challenge. It was to give a type for choose_one that doesn't lead to unsoundness because of a native arity mismatch. See William's first email from the 18th. But I think William's right that there are better pathological cases for your scheme. Once I get you to admit that the inlining is mandatory. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
