On Sat, Feb 21, 2015 at 1:38 PM, Keean Schupke <[email protected]> wrote: > 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.
Not sufficiently helpful. >> 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'. That can't be right. The third argument will be a bool. Did you even read the message I referred to? Rhetorical question. I'm fed up for now. >> 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. But you said "I think that we can consider the specialisation just a form of inlining.". You are right, Keean, you are not good at explaining this. This is your shortcoming, if you're trying to help. I'm done. We're not getting anywhere until you put more effort into making a self-contained explanation of your proposal that is not woefully incomplete. Maybe someone else would like to take a turn coaxing a real proposal out of Keean. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
