On Wed, Feb 25, 2015 at 9:10 AM, Jonathan S. Shapiro <[email protected]> wrote:
> 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.
Aww, you broke my funny reply.
Look, I didn't know what you thought you meant by maximum arity. Based
on your correction, it looks like you mean maximum total arity, which
is indeed unknown in that example. But I really am talking about
maximum _shallow_ arity, which is not the same.
>> >> 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.
Well I'd ask you now to keep the "maximum" and "shallow" bits in mind,
but let's make sure we understand the difference on the other branch
of discussion first. The one with ('ar := 1) vs. ('ar := 1 +
'newArity).
>> 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.
OK.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
