On Mon, Jul 21, 2014 at 11:44 AM, Jonathan S. Shapiro <[email protected]> wrote: > 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.
By implicit, I meant the programmer doesn't write them. I agree that it's necessary to know (statically or dynamically) that array accesses are in range. Another option would've been if the range check is not part of array accessing, but we require the index to be in range. If this is too hard to prove statically, the programmer can manually add a range check, which makes the static check easy. I'd say this second approach is preferable if (and only if) range checks could usually be compiled out in your approach. > 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. Great! Tell me about it! > 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. Part of telling me about preconditions should be explaining why you also need Nat kind. I understand why they're different, but I don't understand why you need both. Incidentally, if you really want both, dependent types are a slick way to reduce them both to a single feature. >> Does BitC actually have an effect or mode or something to rule out >> dynamic checks? > > Indirectly, yes... The rest of your reply basically makes sense to me. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
