On Mon, Jul 21, 2014 at 12:07 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Sun, Jul 20, 2014 at 11:43 PM, Matt Oliveri <[email protected]> wrote: >> 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. > > This is a question that should probably be raised on LtU.
But anyway, you still think it's important? >> 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. > > Our target user base will reject outright any language that requires manual > proof discharge. We can sneak some things in via type level computation, but > they have to discharge automatically in all but the weirdest corner cases. What's the story with preconditions, postconditions, and assertions, then? They will discharge automatically too, or they are an exception to the automatic discharge requirement? Are they part of the language, or just a hook for external tools? I'm not trying to be difficult; the assertion system seems like the closest thing you've mentioned to what I want. >> I'm sorry, but it's not my fault "complete" means many things. > > I agree. But in a conversation about type systems you don't drag another > definition in to confuse the issue. Or if you must, you annotate it. I'd be glad to. Last time, I asked what we should call it. For now, I'll call it Fred. >> For >> deductive systems, "complete" means that a statement is provable >> whenever it's true in all models. > > Which (I think) is isomorphic to the notion of complete types. If inferences > is viewed as a process of deduction, complete types are those that satisfy > all of the possible deductive models. I don't think Fred has much to do with complete types. Complete types seem like a concept for type inference, and Fred makes sense for any Curry-style type system, even if type inference, or even type checking, are impossible. I know you want type inference, but trying to jam ideas from that literature into a conceptually separate issue is not helping. It may be that complete types are also an instance of the notion of a complete deductive system, but I'm pretty sure that would still make them a different instance than Fred. >> 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. > > MOST DEFINITELY NOT. We need to be very careful to distinguish between the > language definition and the artifacts of some particular implementation. > Critical systems should never be written to a particular implementation of a > language. Please read what I said again: "whenever its compiled code has the required properties for *any language implementation*." In other words, if there's any conceivable implementation that would _not_ work a certain way, we do not expect to be able to show in the abstract that it works that way. (And by soundness, we had better _not_ be able to. But this is completeness.) That statement quantifies over all possible implementations deliberately to avoid saying anything about a particular 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. > > Well, no, they really aren't. Because the inference process and the type > system are co-specified as a set of type judgments that cover all of the > operations and forms in the language. The only way inference can fail to > produce a sound and complete typing is if there is some aspect of inference > that is not syntactically directed. You can actually go a bit further than > that. E.g. '.' in BitC is partially type directed, but the inference of the > left-hand side never depends on the right-hand side, so this devolves into > an ordering constraint. Some other forms of type-directed inference would > not be OK in that way. It sounds like you're saying that to get type inference working, in practice you cannot separate the design issue of getting sound and complete type inference from the issue of getting a sound and complete type system. If so, then I am afraid you're right, and it's why I think sound and complete type inference is a bad goal. But that's not what I was saying. Sound and complete inference are soundness and completeness of the type checking/inferencing algorithm with respect to the typing rules. Soundness and completeness of the type system itself is soundness and completeness of the typing rules with respect to the semantics. These properties can all fail independently. Fred is completeness of the typing rules w.r.t. the semantics. This property is nontrivial in the presence of Curry-style types. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
