A module which uses division can operate on positive number types, so the check need only happen once at time of conversion. Clients of such an abstraction would also be forced into using these positive integers.
The arguments below for a dependently typed code are compelling though. Sandro Mark Miller wrote: > 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 >> >> > > > _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
