On Tue, Mar 31, 2015 at 5:01 AM, Keean Schupke <[email protected]> wrote:
> On 31 March 2015 at 09:22, Matt Oliveri <[email protected]> wrote:
>> No, I didn't assume otherwise. Combinations of cfns and HM arrows are
>> not enough to express the necessary constraints. Please do look at the
>> example and consider what could happen in your type system.
>
> Sounds like it would be useful to do this, which example did you mean? Could
> you restate it simply?

This one:

On Tue, Mar 31, 2015 at 12:58 AM, Matt Oliveri <[email protected]> wrote:
> So for example, we get some function f from outside the compilation
> unit, and we apply it like
> f a b
> and
> f a b c d
>
> And both results are passed to other functions outside the unit. What
> type is f, and how do we know that when we specialize these
> applications, we don't insert any lambdas? (This is Shap's example.
> It's a slightly harder version of apply2.)
>
> I figure f has type ('a->'b->'c->'d->'r) in your system. The problem
> is that this seems to have ('a 'b 'c 'd=>'r) as an instance, and we
> can't apply that to two arguments without inserting a lambda.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to