I want to interrupt the discussion very briefly.
Keean is pushing very hard to have a clean and sensible type system. I'm *very* glad to have the view represented here, though not for Keean's reasons. I think that better type systems provide value for systems code that goes well beyond [various forms of] safety. One of the great strengths of this list is that we have always had people here who are willing to argue for the "types should not encode implementation" point of view, but who have also been willing to talk about how implementation issues can nonetheless be practically achieved. It isn't the strength of type theory *or* the strength of implementation that makes the BitC effort interesting. It's the commitment to coherently merge those two things. Matt is starting to try to explain to Keean why implementation issues and type theory are equally first class in BitC. In fact, if we are forced to choose, we're going to choose direct expressibility of performance over clean type theory. Since Keean is pretty new to this discussion, I want to pause here long enough to say that the present debate is actually deeply important, and we cannot have success if the opposing perspectives are not represented. The list is going to push back, Keean, but we need you. [At least] two things are required of a systems programming language, Both are difficult to pin down precisely, but both are essential: 1. The ability to write programs whose concrete behavior on the real machine is transparent. As part of this, the ability to write programs that are low-level expressive **in the absence of optimization**. 2. The ability to write programs that have utterly known behavior with respect to certain kinds of effects, most notably allocation. An implied consequence of these is that BitC categorically rejects approaches that start with "you can start with this high-level thing and optimize your way to that low-level thing". We certainly want strong optimization, and we'll take it wherever we can get it. The problem with these approaches in a systems language is that (a) they fail the test of *direct* expression, and (b) even if they didn't, those optimizations cannot be applied 100% of the time. The second point is deadly. It leaves us in a state where (e.g.) we may not be able to write non-allocating programs because some obscure failure of the current optimizer was unable to eliminate a high-level construct. Put another way: it isn't good enough if a sub-program is (e.g.) non-allocating by virtue of optimization. We require the ability to write sub-programs that are non-allocating because they are *guaranteed* to be non-allocating by virtue of the language specification. Specifying optimizer behavior is beyond current feasibility. A functional language that cannot directly express low-level efficiency is still a useful functional language. A systems language that cannot directly express low-level efficiency isn't useful for *anything*. Of necessity, systems languages deal with implementation and representation, which means they are inherently complex, and to some degree ugly. That complexity is only tolerable if low-level expressiveness is achieved. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
