I have been having an extended conversation with Tim Sweeney, and I think he has convinced me that I was wrong about dependent typing, and therefore wrong about a couple of things in BitC. I have also been reading the technical notes for Deputy, which I had not previously had time to do. All of the arguments below that I attribute to Tim are paraphrased and somewhat extended, so please take any mistakes to be mine.
Tim argues that ground operations should not introduce dynamic checks. That is: operations like array access should *not* implicitly raise an exception when the argument is out of bounds. They should instead be dependently typed, and the programmer should be responsible for explicitly introducing the required checks when the solver cannot discharge the dependencies automatically. There are several parts to the argument: - If dynamic checks are built in to the core runtime, they cannot later be removed by the programmer, and they may significantly impede code generation. - In any case where the core runtime would have specified a check, it is no more expensive to have the programmer write that check. In many cases, exposing the check to optimization will make it cheaper. - Burying an exception raise in the core runtime has the effect of hiding something that the developer may want to see. By making errors silent and invisible, the language inadvertently deprives the programmer of the opportunity to restructure their code to avoid such errors. Tim's language includes a locally inferred dependent type system, and makes it a static compilation failure when dependencies cannot be discharged local to the procedure. In Tim's language, the programmer can then resolve the problem by introducing a dynamic cast, or (I think) by explicitly adding a dependent type declaration to parameters and/or return values. The Deputy language (http://deputy.cs.berkeley.edu/) takes a related approach. Deputy implements a flow-sensitive dependent type system, and automatically introduces dynamic checks whenever the solver cannot solve the constraints directly. Where Tim's approach is strictly static, Deputy's approach is a hybrid checking approach. The advantage of Tim's approach is that it makes potential errors explicit. The advantage of Deputy's approach is that it lowers the programmer burden while exposing core constraints to the optimizer. What I particularly like about both approaches is the notion that dependent types are *locally* inferred, but are not automatically propagated past [top-level] procedure boundaries. This resolves my main concern about dependent types, which is that constraints tend to propagate in expanding and confusing ways. It also resolves my concern about introducing generalized region types into BitC. If the goal is to avoid confusion, the requirements are (a) to use these features judiciously, and (b) to ensure that the absence of constraint annotation is always sensible, in the sense that either (i) it is interpreted conservatively or (ii) whatever interpretation is given is enforced by the compiler. The potential problem here arises when one programmer makes use of dependent typing or regions and another doesn't want to. Deputy offers an obvious solution: make conservative assumptions where the weak use occurs, and either accept a conservative static typing or (where possible) insert a static check as an option. For a variety of reasons, I like the idea of integrating a dependent type system into BitC if we can do it. There are a *lot* of properties one can express that way which can be discharged successfully in suitably designed codes. That said, I do not want to delay the initial release of BitC, so I'm going to classify this one as "this is an area where future language revisions may become incompatible in some way that requires additional annotation. Sheesh. Next Tim will convince me that Monads are a good idea... shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
