On Mon, Feb 23, 2015 at 10:24 AM, Keean Schupke <[email protected]> wrote:
> > f :: fn 3 'a 'b 'c -> 'd >>> >> >> I didn't ask what type you inferred. I asked what syntactic element[s] >> justified your use of the relevant inference rule. If the concrete type of >> f turns out to be: >> >> fn 2 'a 'b -> fn 1 'c -> 'd >> >> >> then your proposed inference is just. plain. wrong. It will place >> parameters in the wrong registers. The whole point of types is to avoid >> having programs that "go wrong" in this way. ;-) >> > > Erm, but I have just said the concrete type is: > > fn 3 'a 'b 'c -> 'd > > That is the concrete type of the application. We can then specialise the > definition by _removing_ lambdas, or specialise the application by > inserting applications. > Yes. You said it. But that's a proof by strong assertion rather than an answer to my question. You are talking about inferring arity at an application. It's important to work the problem all the way from the beginning. Here is the actual application: f a b c Explain what aspects ***of the syntax*** justify the inference that f is an arity-3 function. You may not appeal to any other information. In particular, you do not get to assume any knowledge of how f is defined. As far as I can tell, you can infer that the arity of f is *bounded* by 3, but not that it *is* 3. > At the point of application we know the concrete definition type. > Perhaps I missed something that you said somewhere, but so far as I can determine there is absolutely nothing here that tells me anything at all about the concrete type of f. You don't know the static definition, and if you actually *had* the concrete type of f you wouldn't be *inferring* it. So no, I don't agree that we know the concrete definition type based on the information you have provided. > The subtyping relation I proposed is sound as we can _either_ specialise > the application by inserting applications or specialise the definition by > deleting lambdas. > We can't always delete the lambdas, because in some cases the function being called will be binary-only, and we cannot rewrite those cases. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
