On 24 February 2015 at 15:33, Keean Schupke <[email protected]> wrote:
> > On 24 February 2015 at 15:30, Matt Oliveri <[email protected]> wrote: >> >> upcast1_1to2 f = \x y.(f x) y >> downforce2to1_1 f = \x.\y.f x y > > > Why is that necessary? > > If this is true then you cannot go up or down, so there is not point in > arty-abstract functions at all, as you cannot alter the arity without > inserting lambdas. > There is definitely some weird assumption here, like you are trying to define a coercion to fit into an existing type system or something. You are tying to define a unary coercion that can be used like this: f (upcast1_1to2 g) But that is not at all what we are doing here. There is no need for the coercion to be a unary funciton, remember that both 'f' and 'g' are still arity-abstract in the implementation, so we can specialise them iff they pass the subtyping test. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
