I'm not sure what you mean by "at a certain type". It is a hard requirement that certain programs incur zero dynamic exceptions, therefore zero dynamic checks. It is not realistic to expect that the necessary degree of static analysis will be feasible for all programs.
One of the things about dependent types that concerns me is that you get progressively deeper into black art prover work when you need to achieve this "zero dynamic check" requirement. You obviously have discharge requirements with more ordinary static type systems, and some of those are very challenging in the general case (e.g. range analysis). My concern with Dependent types is that every time you have a type that depends on a [dynamic] value, you introduce a new proof obligation that is potentially very complex! and it's hard to understand when/where you did that. There is a lot we can usefully say with kinding. For now that may need to be enough. If you can explain your question a bit more, I'll try to answer tomorrow. Oh! Are you simply asking what primitive operations incur dynamic checks? shap On Monday, July 14, 2014, Matt Oliveri <[email protected]> wrote: > On Mon, Jul 14, 2014 at 12:42 PM, Jonathan S. Shapiro <[email protected] > <javascript:;>> wrote: > > Matt, I don't mind you expressing your concerns or your philosophy, > though > > you really do need to learn how to differentiate assumptions from facts. > > OK, lets try this again. > Shap, in BitC as you currently envision it, under what circumstances, > if any, will it be impossible to write a program at a certain type, > without incurring implicit dynamic checks, even though the > corresponding untyped program satisfies the semantics of the type in > question? > _______________________________________________ > bitc-dev mailing list > [email protected] <javascript:;> > http://www.coyotos.org/mailman/listinfo/bitc-dev > >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
