What about division by zero? All these same arguments would seem to apply, but it's hard to imagine following through on the implications.
On Sat, Jan 10, 2009 at 10:15 AM, Jonathan S. Shapiro <[email protected]> wrote: > 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 > > -- Text by me above is hereby placed in the public domain Cheers, --MarkM _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
