On Tue, Feb 24, 2015 at 11:55 PM, Matt Oliveri <[email protected]> wrote:
> 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. :) > Ha! Yes, I did say that, but of course I was wrong, because in our example 'a might unify to 'b->'c, so the first step of my proof by contradiction is invalidated. If the type is arity-abstract, and the return type can still unify with a function type, then we haven't established a natural arity yet. > >> 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? > I can try. :-) Unfortunately, given that I got the first part (above) wrong, I do not agree that "it's an instance of" constrains the arity to 2. > What are some of your favorite concrete types? > Well, Sakrete is good for a lot of things... (http://www.sakrete.com) I'd use int or char or string. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
