On Tue, Jul 15, 2014 at 11:26 PM, Matt Oliveri <[email protected]> wrote:
> On Tue, Jul 15, 2014 at 10:30 PM, Jonathan S. Shapiro <[email protected]> > wrote: > > > Given > > complete typings, unique typings are almost a necessary consequence. > > That sounds interesting, let me think about it... > Wait, I thought your "complete" means "maximal with respect to > inclusion". Being maximal would be vacuous if there's only one type to > pick from. In other words, given unique typing, _all_ types are > complete. > I don't think that's correct. For example: in a system having subtypes, there may be several choices in a given type hierarchy under which the program will operate without violating any rules. Complete typings require that you take the maximally inclusive type. But this also identifies a flaw in what I said initially. We take it for granted in HM-style inference that a non-unique resolution (modulo subtyping) is an erroneous inference result. Clearly there are cases where a program can have two valid typings, neither inclusive of the other. In HM-style inference we generally consider such a program to be ill-typed. This is part of why MSL has + vs. +. This sounds similar to the point I made earlier about choosing a type > being like choosing a specification, and that it generally needs to be > a human act of design. Or am I misunderstanding? > I don't think you are misunderstanding, but I think you are raising a false dichotomy. In a language with inference one remains free to declare and thereby proscribe. > > And note that by the time you are generating code you are dealing with > > concrete types, not complete types. > > By concrete types, you mean no type variables? Why would this be? And > how are concrete types opposed to complete types? They never overlap? > Concrete types as in the types actually known to the primitive hardware. Which certainly excludes type variables. If you are generating machine code, the machine type space is the only space you get. > I mean that they are "black art" in the eyes of a systems programmer who > > probably can't name a prover, never mind drive one. > > Ah. I wouldn't have used that term. Even many proof assistant drivers > consider some of Coq's features to be black magic, and that's the kind > of thing I thought you meant. And just generally, it shouldn't be the > case that everything unfamiliar might as well be black art. > Fair enough. And I agree that it's an abuse of the term. Can you suggest a better term? > > I'm pretty firmly on the side of type erasure. So far as I can determine, > > all parts of the BitC type system should be erasable without altering the > > meaning of the program. > > To my ear, that can't be right. For example, integers and interface > instances would be implemented differently. (I hope.) But that > difference was directed by them having different types. > Why would this be so? I'm confused. The erasure property says that you can erase the types *after* performing the checks. Or do you mean that this isn't correct for *qualified* types, because if you erase the qualification you have erased knowledge that is needed to implement the associated *ad hoc* polymorphism? > > > 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. > > The check can be optimized away if the type information tells us enough, > but > > optimization does not change the program semantics. > > That's clever, but it doesn't help if you can't recover from a failing > range check. I guess in BitC it's still up to the programmer to catch > their mistakes. > Yes. For critical code you need to eliminated all of the mistakes you can and then catch the ones you cannot. > > >> 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. > > > > Or we could simply refer to the proof of sound and complete typing for > the > > language core that has already been done... > > By "complete" here, you just mean it'll find a type (maybe even a > complete type) for every program that has one, right? That's not what > I mean. Again, I'm not talking about algorithms here. Then please say what you *are* talking about and stop abusing technical terms that already have firmly established meanings in the literature. I'd like to understand you, but your abuse of terminology is making that difficult for me. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
