On Tue, Feb 24, 2015 at 4:15 PM, Keean Schupke <[email protected]> wrote:
> On 24 February 2015 at 21:11, Jonathan S. Shapiro <[email protected]> wrote:
>> On Mon, Feb 23, 2015 at 2:11 PM, Keean Schupke <[email protected]> wrote:
>>> and we know that you can apply a more-curried function where a
>>> less-curried one is expected, so with the order on types we know:
>>>
>>> fn 1 'a -> (fn 1 'a -> 'a)   is acceptable where fn 2 'a -> 'a -> 'a is
>>> expected, and we can make it work by removing lambdas form the definition,
>>> or adding applications to the call site, which represents moving from one
>>> type to the other, but in opposite directions.
>>
>> Another way to say this, which does not appeal to sub-typing, is that we
>> can infer your application f 1 2 to have the type
>>
>> ('arity <= 2) =>   fn 'arity 'a -> 'a -. 'a
>
> This is probably saying the same thing... but it ignores deeper arities.
>
> The other side is the definition defines the lower bound on arity so you
> might have:
>
> ((1, 1) <= 'arity <= (2)) => fn 'arity 'a -> 'a -> 'a
>
> And then you are kind of doing the same thing, but with a more complex type
> system...

But it _isn't_ doing the same thing. That's what I've been trying to
tell you. It deliberately rules out coercions.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to