On Wed, Feb 25, 2015 at 12:37 AM, Jonathan S. Shapiro <[email protected]> wrote: > 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.
So whereas I claim that it has a maximum arity of 2, you argue that its arity is at most 2. :) >> 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. Shap, I'm talking about *maximum* arity. I'm well aware that we don't know the actual arity yet. I think there's still an issue lurking here, so can you reconsider what I said, keeping the "maximum" bit in mind? > 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. Sorry, I was just pretending Nat was a type for the purpose of illustration. I forgot it would clash with the Nat kind because I'm used to dependent types. I probably got the naming convention wrong too. What are some of your favorite concrete types? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
