On 12 February 2015 at 20:52, Keean Schupke <[email protected]> wrote:
> > On 12 Feb 2015 09:21, "William ML Leslie" <[email protected]> > wrote: > > > > f : Nat -> Nat -> Nat > > f x y = ... > > > > g : {X} -> (X -> Nat) -> X -> Nat > > g f x = f (S x) > > > > let h = (if something then f else (g f)) in ... > > > > both f and g have the same type, but different native arities. The > question is, what is the native arity of h? There are two sensible > answers. Of the usages of h that might follow, we may have a hard time > deciding which to make first-class. When h is a local, it might even be > sensible to provide both immediately. > > Either f and g have the same type, in which case they are substitutable > for each other, or they don't. I don't get your interpretation of type. > Ah, see this is the point. From the perspective of the language user, you may remain blissfully aware that f and (g f) have different native arities. They are completely substitutable. As a compiler, you will do your best to avoid any unnecessary thunking. You're going to emit calls to a statically-determined f as two-argument calls, or you're going to wrap f in a function that performs currying, where it's underapplied. And you're going to emit two call instructions whenever you see (g f) called - one to call g, and one to call the result. This is what Geoffrey means when he asks about the implementation of multi-argument functions. Systems programmers have a need to reason about when the unification expressed in `h` above introduces allocation and when it will have an impact on the performance of calls to h. > > In the specific case of type systems for calling conventions, there is > "Types Are Calling Conventions" by Bollingbroke and SPJ, as existing work. > BitC's intended audience has additional bearing on this, and that is what > we're trying to discuss. BitC cannot entertain the same level of magic as > other languages might be able to get away with. We want native performance > out of what may be generic or higher-order calls. > > I disagree with this. The type system has nothing to do with the > implementation. I think you can have c/c++ performance with a 'magic' type > system. > You can represent many implementation features with type systems. For example, MLkit's region types were really never visible to the user. Yet, they were a type system, and they were useful. They attached information to a program location, information that propogated in a well-defined static way, that was ultimately used in the translation to machine code. That is the nature of a type system for calling conventions. -- William Leslie Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
