On Mon, Jul 21, 2014 at 12:46 AM, Jonathan S. Shapiro <[email protected]> wrote: > 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. +.
So what you're saying is that given complete typings, the complete types are unique? This is not to say types are unique, just that all the other types an expression has are not complete. Unique types would be if there's really only one type for an expression; guess which one is complete. ;) (And technically, this is all up to some appropriate type equivalence relation.) >> 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. I didn't mean to say a language with complete inference shouldn't allow type annotations. But what I was implying is that if type annotations are needed in practice, I don't understand why it's so important for the inference to have any theoretically-good properties. >> > 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. OK. >> > 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. >> >> I wouldn't have used that term. > > Fair enough. And I agree that it's an abuse of the term. Can you suggest a > better term? Well here's an opportunity to clarify: Do you mean proof goals the user could end up dealing with, or proof goals the compiler has to somehow handle automatically? I propose "proof handling" and "theorem proving", respectively. >> > 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. I was being an idiot. "Erase" is not what I should've said at all. I think there is something right I could say, which is what I was trying to say, but I don't know how to explain it. At any rate, Curry-style types are basically just extra tacked-on information about an existing thing. > 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? Nope, nothing so complicated. Just a terrible word choice. >> > 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. Does BitC have a way to try to statically rule out all dynamic exceptions? >> >> 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. I'm sorry, but it's not my fault "complete" means many things. For deductive systems, "complete" means that a statement is provable whenever it's true in all models. This is the closest idea I know to what I'm getting at: that a program has a type whenever* its compiled code has the required properties for any language implementation. Basically I took the special case of Curry-style types as a deductive system about programs. Soundness and completeness of a type system are different from soundness and completeness of type inference. But what would you like to call this property? * Gödel's incompleteness theorems make this impossible in interesting cases, so we'll settle for almost complete. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
