On Tue, Jul 15, 2014 at 11:47 PM, Matt Oliveri <[email protected]> wrote:
> On Tue, Jul 15, 2014 at 10:30 PM, Jonathan S. Shapiro <[email protected]> > wrote: > > I don't agree with you about punting to dynamic checks, since (e.g.) the > > range check on array bounds is defined to be part of the accessor > operation. > > This is actually important. If you're OK with regularly punting to > dynamic checks then completeness isn't hard after all. I guess I > assumed (yes) you considered implicit dynamic checks to be > undesirable. > They explicit rather than implicit (because they are specified behavior), and they are necessary. So far as I can remember, there are only two exception-raising operations: integer divide by zero and vector bounds violation. Both are things that can be compiled out if we adopt preconditions. The vector exception is the interesting one, because if the argument presented has Nat kind we can often see that no bounds check is needed. I haven't figured out the right way to overload [] yet, but my guess is that we're going to end up with []: vector 'a X Nat -> 'a // never throws, bound is statically discharged []: vector 'a X Word -> 'a // throws on bounds violation But I haven't got this issue worked out yet. Does BitC actually have an effect or mode or something to rule out > dynamic checks? Indirectly, yes. The plan is to have an effect "nothrow" (needs a better name). The meaning of this is that calling a procedure will not result in an exception that escapes that call. The procedure can still use exceptions within its internal behavior, provided all such exceptions are caught. This actually isn't adequate, because we aren't surfacing exceptions in the type signatures. Also, "no exceptions" isn't the same thing as "cannot raise", so the two issues may want to be separated. > I seem to remember some discussion of a no-throw > effect. How do you deal with the [range check is part of the > operation] approach there? If the range check can be statically discharged, then the vector index operation is deemed not to throw. If we cannot discharge the obligation statically, then a throw is possible and the no-throw type constraint fails to type check. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
