On Tue, Feb 24, 2015 at 10:37 AM, Keean Schupke <[email protected]> wrote: > 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.
For some reason, I received this email later than your more recent ones. The coercion needs to work in a system where arities must match exactly, since--as I understand it--your proposal is relying on them to provide arity subtyping in the first place. To assume arity subtyping or similar when implementing the coercions would be begging the question. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
