On Tue, Feb 24, 2015 at 8:55 PM, Matt Oliveri <[email protected]> wrote:
> But none of that seems to address what I'm asking about maximum > (shallow) arity. How can we tell that the maximum arity of (fn 'arity > Nat->Nat->'a) is 2? You can't. You only know that it is **bounded by** 2. You now this because this type was inferred constructively over well-formed program fragments. Proof sketch by contradiction: 1. Suppose the native arity were greater than 2. Then it would follow that there must be three or more arguments before the final type. => contradiction 2. Since all functions take at least one argument, you now it is at least 1. > How about (fn 'arity Nat->Nat->String->Float)? As > an instance of the previous one, it should still be 2. In the mode I have in mind, this instance-of argument is incorrect. > But of course > that type could be inferred from some other application... No! In principle, concrete arities for the applied function are not inferrable from applications. Aside: In BitC, Nat is not a type. It is a kind. It would be helpful if you could use examples that do not mix type orders in this way. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
