On Thu, Feb 12, 2015 at 10:09 AM, Jonathan S. Shapiro <[email protected]> wrote:
> On Thu, Feb 12, 2015 at 12:27 AM, Matt Oliveri <[email protected]> wrote:
>>
>> I'm not sure what you're saying we should infer for the (f x y)
>> example. That could either be a 2-application, or two 1-applications,
>> if they had the same syntax. That's why I proposed writing two
>> 1-applications like ((f x) y).
>
>
> So if we want to get detailed about it, (f x y) probably means that we infer
>
> 'arity <= 2 => fn 'arity 'a -> 'b
>
> The nat in the fn type has nat kind for a reason!

I didn't think it was so complicated. I certainly didn't intend to
propose something so complicated. The syntax (f x y) is well-typed
only if f has arity 2. Option 1 _was_ "arity must match".

You gave an example:
> This, incidentally, implies that even if we end up using curried
> application *syntax*, the application
>
>  f a
>
> will signal a type mismatch if the arity of f is something other than 1
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to