As in a current language, division could take a pair of rational numbers and return an option type containing a rational number, and the caller would be responsible for explicitly handling both cases of the result. You could write this as:
divide(numerator:Rational,denominator:Rational):Maybe(Rational) Or, if the type system includes a feature equivalent to intersections and complements, it could take a pair of a rational number and a non-zero rational number, and return a rational number. You might write this as: divide(numerator:Rational,denominator:Rational!=0):Rational And then the caller would be responsible for guaranteeing it's called with a second argument which the compiler can prove is nonzero. Examples that the compiler accepts: pi = 22/7; f(x:Rational!=0)=22/x g(x:Rational)=if(y:Rational!=0 = x) then 22/y else 0 In the case of "g", we're passed an arbitrary rational number and must explicitly check whether it's in the type Rational!=0. If this is the case, the binding-conditional statement uses x to initialize a new variable y known to be a Rational!=0, and otherwise it falls through the the "else". As a result, there is never a case where the compiler silently introduces an exception or runtime error into user code. If you write: h(x:Rational)=22/y then you get a compile-time error. -Tim P.S. Monads are a great idea for expressing operations analogous to iterators and database queries within a pure functional language. The bad idea in Haskell was applying them to general imperative programing a la Haskell IO/ST monads. ________________________________________ From: [email protected] [[email protected]] On Behalf Of Mark Miller [[email protected]] Sent: Saturday, January 10, 2009 2:14 PM To: Discussions about the BitC language Subject: Re: [bitc-dev] Hybrid dependent typing 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 _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
