To expand on my last point, I think a pure lambda calculus can model any computation. I think a type system restricts the admissable lambda terms to a subset with your desired semantics. I think you can then directly compile that semantics.
For example starting from a pure lambda calculus you can have a type system that admits terms with the same semantics as C (in this case all C statements would be in something like the IO monad). You can then compile this directly to assembly in the same way a C compiler does. The lambda model and type system can be viewed as a validation stage, but then maybe the C compiler can use this model to improve optimisation beyond what a normal C compiler is capable of by tracking aliasing for example. Maybe this isn't right for BitC, but I think it is worth mentioning. Keean. On 12 Feb 2015 09:52, "Keean Schupke" <[email protected]> wrote: > > On 12 Feb 2015 09:21, "William ML Leslie" <[email protected]> > wrote: > > > > On 12 February 2015 at 19:56, Keean Schupke <[email protected]> wrote: > >> > >> You can infer the required type of 'f' from its use. > >> > >> You can also infer the defined type of f from its definition. > > > > The issue under discussion is not about types (at least, not in the > usual sense). Consider: > > > > 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. > > > > > > >> > >> You can treat this compositionally, so when two program fragments are > composed, you match the requirements from one fragment against the > definitions from the other. > > > > We are familliar with how a type system works, you know. > > Actually most type systems are not compositional, and I don't think many > non - intersection type systems gave principal typings (note, different > from principal types). > > > 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. > > Keean. >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
