On 31 March 2015 at 14:32, Matt Oliveri <[email protected]> wrote:
> 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.
>
>
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
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)
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
Keean.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
