On 21 Feb 2015 13:39, "Matt Oliveri" <[email protected]> wrote: > > 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,
Just read the curly brackets as named implicit variables, so they not only have to match the type in the environment but the symbol name too. > 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. Choose one gets the following type I think: fn (fn 'a 'b -> 'c) (fn 'a 'b -> 'c) (fn 'a 'b -> 'c) -> 'c Inferred from the application of 'f'. > > 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. The inlining does not seem mandatory because you can just specialise the call instead, which I think is what shap was proposing. You have the concrete defined type, and the concrete type inferred from the application, and you can specialise the definition or the application, providing the partial order on types is followed. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
