On Tue, Mar 31, 2015 at 10:53 AM, Keean Schupke <[email protected]> wrote:
>> 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.
>
> If we get a function from outside the compilation unit, then we also get its
> defined type signature.
>
> I would infer for the first:
>
> f : a -> b
>
> I would infer for the second:
>
> f : a -> b -> c -> d
You probably mean (f : a->b->r) and (f : a->b->c->d->r), since the
applications had 2 and 4 arguments, not 1 and 3. But I see what you
mean. I'll use your types.
> Because I have a multi-set environment we can happily have {f : a -> b, f :
> a -> b -> c ->d}, which you could also write using intersection types as f :
> (a -> b) & (a -> b -> c -> d)
Interesting. This doesn't seem to solve it though, since (a->b) and
(a->b->c->d) unify to just get (a->b->c->d). So the intersection isn't
telling us anything new. If that's unintuitive, it might be because
you really do want a call arrow but didn't realize it!
> The imported type of 'f' must unify with both of these, so valid types
> would be:
>
> f : a -> b -> c -> d
> f : a => b -> c -> d
> f : a => b => c -> d
> f : a => b => c => d
> f : a => b c => d
Why isn't (f : a b c => d) valid? It unifies with (a->b->c->d), (and
therefore (a->b)) doesn't it?
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
