Keean: You are right in that you don’t need a general unary function to do this.
However, we do need to /transform/ the input language L with arity-abstract function definitions and applications into a language M without. Part of the difficulty here is how you describe this transformation. In other words, describe exactly what Shapiro means with “AST manipulation”. In addition, typing rules needs to be specified so that a) we can allow/disallow allocations, and b) so that we can check that arities are correct and c) so that we can infer information from the code (such as exact arities). Would you mind elaborating on what your proposal is in this context? In other words, in addition to describe typing rules also specify translation rules (for function definitions, function applications and finally function values)? I have a hard time seeing what you actually propose. To me, it is interesting to look at the case where we have a term `f x y`, where f is passed in as an arity-abstract parameter. How exactly would you transform that term (in language L) into a term in language M? Thanks, PKE From: bitc-dev [mailto:[email protected]] On Behalf Of Keean Schupke Sent: Tuesday, February 24, 2015 7:37 AM To: Discussions about the BitC language Subject: Re: [bitc-dev] Arity inference at call (application) sites On 24 February 2015 at 15:33, Keean Schupke <[email protected]<mailto:[email protected]>> wrote: On 24 February 2015 at 15:30, Matt Oliveri <[email protected]<mailto:[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
