On Tue, Jul 15, 2014 at 12:14 AM, Jonathan S. Shapiro <[email protected]> wrote: > I'm not sure what you mean by "at a certain type".
That technicality is necessary to rule out assigning weaker types to "the same" programs. It's hard to state this question in general for all systems. For example, what on earth is the "corresponding untyped program" in general? If BitC has unique typing, then technically different types contain disjoint sets of programs. But unique typing is kind of unintuitive to me for a strong type system. > 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. That's actually a great point for my side of the argument. How are you going to get the right types while avoiding unacceptable dynamic failures, for all programs, when (automated?) static analysis is generally infeasible? > 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. Well the proof obligations can get arbitrarily bad, but that doesn't technically mean you need to resort to black art features. Many people choose to do so for productivity. I actually try to avoid it. At any rate, the extensible proof checker approach strongly favors justifying prover features, so they aren't such a black art anymore. > 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). Yes. > 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! Well it isn't the dependency per se that causes the proof obligations, but they do tend to go together. > and it's hard to understand when/where you did that. Nonsense. The typing rules tell you everything you'll need to show. Maybe you're saying it's hard to predict when this (innocent-looking) code leads indirectly to that (impossible-looking) proof obligation. That's just a fact of sound type systems though. If you want to claim strong things, someone has to prove them. Dependent types just have a way of making it surprisingly easy to claim strong things. > There is a lot we can usefully say with kinding. For now that may need to be > enough. Can you get decision procedures for all the things expressible with your kinding system? If not, how are proof obligations handled? > Oh! Are you simply asking what primitive operations incur dynamic checks? Not really, but it could turn out to be relevant. > If you can explain your question a bit more, I'll try to answer tomorrow. I guess the question can't even be stated rigorously if your type system doesn't have an intended formal semantics. But the essence of the problem seems to be that many type systems use Church-style typing or dynamic checks when they probably should have used Curry-style or refinement typing. Types can do two things: - Constrain the way values are constructed, thereby possibly guaranteeing some properties by construction - Guarantee properties of values without further constraining the way they are constructed The second thing is refinement types. These also correspond roughly to Church-style and Curry-style typing, respectively. Given a full language, it can be hard to tell which guarantees were "meant" to be provided Curry-style because Church-style can be easier to implement, so it's sometimes used even when it doesn't make so much semantic sense. Worse, this decision can then be exploited by compilers, making it look, from an implementation point of view, like it was meant to be Church-style all along. But the unwanted constraints on how values are constructed can give rise to the intuitive feeling that the language is incomplete, because some value with some property _should_ exist, but there's no way to construct it so that it has the property by construction, which is what the language required. Curry-style typing has no affect on the actual program that runs. Whether a value has a type is just a matter of fact; nothing needs to be done to make it so. So asking which parts of the BitC type system would ideally be Curry-style is kind of like asking what types would ideally be completely erased. There are various ways to set up an intended semantics for a language, but for now what's interesting is that it should show which types are meant to be Curry-style/refinement types. Given an informal sketch of such a semantics for BitC, we could start talking productively about how close to complete BitC's typing rules are. The reason why I assumed BitC would turn out not to be very complete is because I don't know of any practical, safe, typed languages that are. It tends to require a full proof assistant to justify the refinements in general. Punting with Church-style typing or dynamic checks means they're not really just refinements anymore. Questions? Comments? I hope this doesn't seem too far out of left field. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
