ok@cs.mu.oz.au (Richard O'Keefe) (09/27/89)
Once upon a time I thought I knew what "extra-logical" meant in
logic programming circles. I could, for example, turn to
"The Art of Prolog", and find
There is a class of predicates in Prolog that lie
outside the logic programming model, and are
called {\it extra-logical\/} predicates. These
predicates achieve a side effect in the course of
being satisfied as a logical goal.
Sterling and Shapiro explicitly list
transput commands and
program manipulation commands.
[I do wish people would stop talking about SIDE effects when
referring to the MAIN effect of something like write/1 or assert/1.]
The Sterling and Shapiro text offers two definitions, really.
X is extra-logical if
[definition 1] it lies outside the logic programming model
or
[definition 2] it has a ``side effect''.
Under definition 1, I would include var/1 and anything which can be
used to simulate it, such as cut, unsound negation, unsound if then else,
findall/3, even perhaps compare/3 (but not NU Prolog's termCompare/3).
However, Sterling & Shapiro do NOT describe these operations in their
chapter on extra-logical predicates, which suggests that they may not
have intended the word to apply to them.
The reason that I ask is that I was stunned to find a paper which
described the Mycroft/O'Keefe type system as ``extralogical''. Now,
we're talking about a type system where type declarations are
syntactic sugar for certain Horn clauses, and where a predicate declaration
pred p(T1, ..., Tn)
is interpreted as saying that
p(X1, ..., Xn) :- Body
is to be read declaratively as
p(X1, ..., Xn) :- isa(X1, T1), ..., isa(Xn, Tn), Body.
(in essence, the type checks are ``factored'' out into the declaration.)
I really can't see any side effects there, nor can I see how to simulate
var/1 with this stuff, nor yet does it seem to me to lie outside the
logic programming model. Is there some other sense of ``extralogical''
which does apply? Did presenting the system in proof theoretic rather
than model theoretic terms damn it to extralogicality?
So, what DOES ``extralogical'' mean?
--
GNUs are more derived than other extant alcelaphines,| Richard A. O'Keefe
such as bonteboks, and show up later in the fossil | visiting Melbourne
record than less highly derived species. (Eldredge) | ok@munmurra.cs.mu.OZ.aualberto@tove.umd.edu (Jose Alberto Fernandez R) (09/27/89)
>> The reason that I ask is that I was stunned to find a paper which >> described the Mycroft/O'Keefe type system as ``extralogical''. Now, >> we're talking about a type system where type declarations are >> syntactic sugar for certain Horn clauses, and where a predicate declaration >> pred p(T1, ..., Tn) >> is interpreted as saying that >> p(X1, ..., Xn) :- Body >> is to be read declaratively as >> p(X1, ..., Xn) :- isa(X1, T1), ..., isa(Xn, Tn), Body. >> (in essence, the type checks are ``factored'' out into the declaration.) >> I really can't see any side effects there, nor can I see how to simulate >> var/1 with this stuff, nor yet does it seem to me to lie outside the >> logic programming model. Is there some other sense of ``extralogical'' >> which does apply? Did presenting the system in proof theoretic rather >> than model theoretic terms damn it to extralogicality? Well, your ISA(Term, Type) predicate could be as extra-logical as VAR(Term) is. I think that it. For example, what happen if a variable is not instanciated when the predicate P is called? There are 3 alternatives: (1) The predicate fail, because the variable is not of the type at that time. (2) The variable is assumed to be of the type. No further checking is done. (3) The checking is delayed until the variable is instantiated, at that time the type checking is fired. Only the third option is not extra-logical, because the order in which the predicates are executed does not change the answer. The first 2 options are order-sensitive, that means that if I change the order of the calls in the clause the answer will be diferent (conjuctions are not conmutative) in other words, the denotational and operational semantics can be diferent. Jose Alberto. -- :/ \ Jose Alberto Fernandez R | INTERNET: alberto@tove.umd.edu :| o o | Dept. of Computer Sc. | :| ^ | Univesity of Marylad | :\ \_/ / College Park, MD 20742 |
hawley@icot32.icot.junet (David John Hawley) (09/28/89)
In article <ALBERTO.89Sep27114947@tove.umd.edu> alberto@tove.umd.edu (Jose Alberto Fernandez R) writes: > >Well, your ISA(Term, Type) predicate could be as extra-logical as VAR(Term) >is. I think that it. For example, what happen if a variable is not >instanciated when the predicate P is called? > >There are 3 alternatives: >.... 4) The variable's tag is changed to Type without assigning a binding. Another way of putting it is that the variable is CONSTRAINED to be the given type. This is constraint LP and the CLP implementation techniques apply. Needless to say, it's apple-pie logical. -------- Eat this Pnews semi- intelligent software --------- David Hawley, 1st Lab, ICOT
lee@munnari.oz.au (Lee Naish) (09/28/89)
In article <ALBERTO.89Sep27114947@tove.umd.edu> alberto@tove.umd.edu (Jose Alberto Fernandez R) writes: >>> pred p(T1, ..., Tn) >>> is interpreted as saying that >>> p(X1, ..., Xn) :- Body >>> is to be read declaratively as >>> p(X1, ..., Xn) :- isa(X1, T1), ..., isa(Xn, Tn), Body. > >Well, your ISA(Term, Type) predicate could be as extra-logical as VAR(Term) >is. I think that it. For example, what happen if a variable is not >instanciated when the predicate P is called? The isa predicates are not extra logical. The types are defined in a special language (for expressing regular trees) which can be seen as a syntactic sugar for (a sub-set of) Horn Clause Logic. What is important here is the *meaning* of the pred declaration/isa call. Its meaning is expressed entirely in classical first order logic. Its not possible to do this for var (at least without destroying the closeness of the Prolog-logic connection). What happens when P is called is an entirely different question to the meaning of P. When P is called, the isa calls are not executed at all. The aim of the *compile time* type checking is to ensure that the computed answers (at run time) are correct with respect to the intended meaning of the program (ie, with the isa calls), without having to actually call isa at runtime. I think the Mycroft & O'Keefe work (at least the versions which I have seen), and most other papers on types for Prolog, do not clearly state what the intended semantics of a program with type declarations is. The way I arrived at the semantics was from considering the difference between natural specifications and efficient programs (the specifications include the isa calls, using Richard's notation, whereas the programs don't). Richard arrived at the same conclusion using a different path. lee
jiyang@ecrcvax.UUCP (Jiyang Xu) (10/10/89)
In article <2204@munnari.oz.au>, ok@cs.mu.oz.au (Richard O'Keefe) writes: > The reason that I ask is that I was stunned to find a paper which > described the Mycroft/O'Keefe type system as ``extralogical''. Now, > we're talking about a type system where type declarations are > syntactic sugar for certain Horn clauses, and where a predicate declaration > pred p(T1, ..., Tn) > is interpreted as saying that > p(X1, ..., Xn) :- Body > is to be read declaratively as > p(X1, ..., Xn) :- isa(X1, T1), ..., isa(Xn, Tn), Body. > (in essence, the type checks are ``factored'' out into the declaration.) > I really can't see any side effects there, nor can I see how to simulate > var/1 with this stuff, nor yet does it seem to me to lie outside the > logic programming model. Is there some other sense of ``extralogical'' > which does apply? Did presenting the system in proof theoretic rather > than model theoretic terms damn it to extralogicality? > > So, what DOES ``extralogical'' mean? Okay, I am the one who is most responsible for that paper. To Richard, I have explained a lot in my response to your mail, but have not seen any reply from you. Let me repeat my argument in that mail: --------------------- About your comment on our claim that "types in M&O scheme is extra-logical", I do not see any ambiguity here. In your paper you wrote "type checking does not change the semantics of Prolog", does that mean a program has the same semantics no matter whether there are type declarations existing? If yes, does that mean the type declarations have no semantics? I am not saying the type declarations have no semantics at all, their semantics is not related to (first-order or higher-order) logic. In the sentence following above, you wrote that the type checking "merely discourages the execution of ill-typed programs", but "ill-typed programs" are defined by mimicing traditional procedural languages. -------------------- Now, you claim your type declaration is just a "syntactic sugar for certain Horn clauses". Are you telling me that p(X1, ..., Xn) :- isa(X1, T1), ..., isa(Xn, Tn), Body. _does not change the semantics of_ p(X1, ..., Xn) :- Body. Yes, of course you can _give_ a semantics to type declarations in this way, and in fact this is almost exactly what we did in our LP'88 paper (for other readers, the paper "a type inference system in Prolog", by Jiyang Xu and David S. Warren, Proc. of Fifth ICLP, pp 604-619), and a paper by Lee Naish in 1987. The point is you did not think this way, or at least you did not claim you thought this way. There are several other works that give semantics to type declarations, for example typed unification by Michael Hanus (something similar to typed lambda calculus), order-sorted logic by Gert Smolka and etc., and our partial logic semantics. The discussions and references are all included in our paper which you read. How can one tell _which_ semantics you had in mind? As you can see, all these methods give different semantics to types. Giving semantics to type declarations is not a piece of cake that you can simply _left out_ from your paper as you said in your previous mail. -- Jiyang Xu ========================================== ECRC, Munich, West Germany jiyang%ecrcvax.uucp@pyramid.pyramid.com or jiyang@ecrcvax.uucp ==========================================
ok@cs.mu.oz.au (Richard O'Keefe) (10/11/89)
In article <786@ecrcvax.UUCP>, jiyang@ecrcvax.UUCP (Jiyang Xu) writes: In article <2204@munnari.oz.au>, ok@cs.mu.oz.au (Richard O'Keefe) writes: > So, what DOES ``extralogical'' mean? : Okay, I am the one who is most responsible for that paper. To Richard, : I have explained a lot in my response to your mail, but have not seen : any reply from you. Let me repeat my argument in that mail: I have received other mail from Jiyang Xu and replied to it. I have not, however, received any mail which clarifies this point. : About your comment on our claim that "types in M&O scheme is extra-logical", : I do not see any ambiguity here. In your paper you wrote "type checking : does not change the semantics of Prolog", does that mean a program has the : same semantics no matter whether there are type declarations existing? I say that claim is _wrong_, not that it's _ambiguous_. As I recall it, Alan Mycroft wrote that (he wrote most of the paper). It is an essential property of ML-like type systems that type checking serves only to accept or reject entire programs; once a program has been accepted as well-typed the types are not used at run time. A recent paper on this subject is The Essence of ML John C. Mitchell & Robert Harper POPL 15, 1988 The point is that you have two related languages, a typed language and an untyped language. BOTH languages have a semantics; the point of a type checking theorem is to show that a formula in the typed language can be evaluated correctly by the untyped interpreter. In the case of the Mycroft/O'Keefe system, it is again the case that there are two languages, ***EACH*** with a logical semantics. One of them is the language with type information in it, call it HCMT (for Horn Clauses with ML Types). The other is HC (Horn Clauses simpliciter). The central theorem of the paper is that a program in HCMT can be interpreted by SLD resolution as an HC program, just by erasing the types, and that this preserves the semantics of HCMT programs. To repeat, the essence of the idea is that type checking is a compile time operation whose effect is to reject entire programs, and that the types have no run-time role at all. The type system described in the Xu and Warren paper has exactly the same property! "The type of a predicate [is an] abstract semantics of the regular program semantics". If the fact that types play no role at run time is what makes a type system "extralogical", then the Xu and Warren system is also extralogical. : If yes, does that mean the type declarations have no semantics? No, the type declarations have a first-order logical semantics. The point is that type checking shows that the type goals are redundant, so that they do not need to be executed at run time. It is possible to do this precisely *because* the type declarations have a first-order logical semantics. : I am not saying the type declarations have no semantics at all, : their semantics is not related to (first-order or higher-order) logic. Here is what a type declaration looks like in the Mycroft/O'Keefe scheme. :- type t(T1,...,Tn) --> c1(X11,...,X1n1) | ... | ck(Xk1,...,Xknk). where the Ti are distinct type variables, the ci/ni are distinct constructor functions, and the Xij are terms made up of type variables (which must appear in the head; this is important for technical reasons that I'll not go into) and type constructors, possibly including t/n. Here is the semantics of such a declaration: isa(c1(A1,...,An1), t(T1,...,Tn)) :- isa(A1, X11), ... isa(An1, X1n1). ... isa(ck(A1,...,Ank), t(T1,...,Tn)) :- isa(A1, Xk1), ..., isa(Ank, Xknk). For example, here are two of the predefined types and their meanings: :- type pair(K,V) --> K-V. :- type list(T) --> [] | .(T,list(T)). isa(A-B, pair(K,V)) :- isa(A, K), isa(B, V). isa([], list(T)). isa([A|B], list(T)) :- isa(A, T), isa(B, list(T)). If a compositional mapping from declarations to Horn clauses does not constitute a first-order logical semantics for those declarations, I don't know what does. It's true that the Mycroft/O'Keefe paper doesn't present exactly this mapping, but it does say "Our approach is to consider type specifications as restrictions on arguments to predicates (and functors). ... We do not test for violation of such restrictions at run time, but by statically forbidding all programs which may lead to a type error. ... the well-typing rules ... are essentially Horn clauses." A predicate declaration in the Mycroft/O'Keefe scheme looks like :- pred p(X1,...,Xn). where each of the Xi is a type term. This is "a restriction on arguments to predicates". The semantics is again compositional; every clause p(A1,...,An) :- Body is to be read AS IF p(A1,...,An) :- isa(A1, X1), ..., isa(An, Xn), Body had been written. The net effect is that the combination of - type declarations, - predicate declarations, and - Horn clauses is another set of Horn clauses. The meaning of the declarations and clauses is defined to be the meaning of the Horn clause program which results. For example, consider the HCMT program :- type list(X) --> [] | [X|list(X)]. :- pred append(list(X), list(X), list(X)). append([], L, L). append([H|T], L, [H|R]) :- append(T, L, R). This program has a well defined first-order meaning; which is the same as the meaning of isa(X, integer) :- integer(X). /* other built-in types */ isa([], list(_)). isa([A|B], list(X)) :- isa(A, X), isa(B, list(X)). append([], L, L) :- isa([], list(X)), % drop, because true isa(L, list(X)), isa(L, list(X)). % drop, because redundant append([H|T], L, [H|R]) :- isa([H|T], list(T)), % reduce isa(L, list(T)), isa([H|R], list(T)), append(T, L, R). The clauses for append/3 simplify to append([], L, L) :- isa(L, list(_)). append([H|T], L, [H|R]) :- isa(H, X), isa(T, list(X)), isa(L, list(X)), isa(R, list(X)), append(T, L, R). the last clause of which simplifies to append([H|T], L, [H|R]) :- isa(H, X), isa(L, list(X)), append(T, L, R). Now there is another HC program which can be obtained from the same HCMT program, by discarding the declarations. That's just the append/3 we know and love. That predicate has a DIFFERENT meaning: append(1, 2, [1|2]) is in the meaning of the usual definition of append/3, but it is ***NOT*** in the meaning of the HCMT program *with* the declarations. So we have two different ways of turning an HCMT program into a set of Horn clauses: one which inserts isa/2 goals, and one which just discards the declarations, and these two methods yield DIFFERENT meanings. The type declarations *DO* make a semantic difference. The point is that if you have a well-typed program (a static check) then well-typed *queries* can't DETECT the difference; any query which could detect the difference will be rejected by the type checker. Because of that, you can use (the type checker to screen out ill- typed queries followed by) the untyped program to find the same answers that the typed program would have done. I repeat, the Xu and Warren type inference system appears to have the same character: the types which are inferred do not have any run-time effect. : In the sentence following above, you wrote that the type checking : "merely discourages the execution of ill-typed programs", but : "ill-typed programs" are defined by mimicing traditional procedural : languages. What Alan Mycroft wrote was "Due to the type checker being a separate program, type checking does not change the semantics of Prolog, but merely discourages the execution of ill-typed programs." That is, the type checker was not built into DEC-10 Prolog, so although the type checker could say "this program or query is not well-typed" (and thus change the semantics of the program or query to "no"), it could not prevent you running the program in straight DEC-10 Prolog anyway. I don't see how anyone can get from that to '"ill-typed programs" are defined by mimicking traditional procedural languages'. Alan Mycroft didn't say that, I didn't say it, and it isn't true. Traditional procedural languages don't allow ill-typed programs, and the ill-typed nature of the query ?- append(1, 2, X). has nothing to do with traditional procedural languages. : Now, you claim your type declaration is just a "syntactic sugar for : certain Horn clauses". Are you telling me that : p(X1, ..., Xn) :- isa(X1, T1), ..., isa(Xn, Tn), Body. : _does not change the semantics of_ : p(X1, ..., Xn) :- Body. No. I'm saying that it ***DOES*** change the semantics (in a compositional first-order way), but that for well-typed programs and well-typed queries you can't DETECT the difference. : The point is you did not think this way So now he reads minds. Brilliant. : How can one tell _which_ semantics you had in mind? Reading the paper is a good way. The point is tht Xu CLAIMED TO KNOW what our semantics was and to know that it was "extralogical". Given that the abstract of the paper says explicitly "we observe that the type resolution problem for a Prolog program is another Prolog program" it was obvious that we had _some_ sort of logical semantics in mind. : Giving semantics to type declarations is not a piece of : cake that you can simply _leave out_ from your paper as you said : in your previous mail. I did not say that giving a semantics to type declarations is a piece of cake. Neither did we simply leave it out. The key point, the very most important thing, about the Mycroft/O'Keefe type system, is that it is not original. We didn't have to define the semantics of our polytypes, because we stole them from Milner. The paper was quite explicit that declarations for predicates were to be viewed as restrictions on their solution sets. Re-reading the Mycroft & O'Keefe paper, I have to agree that it doesn't spell things out much. Unfortunately, both of us were PhD students who were supposed to be doing other things, and we thought that everyone understood the ML type system (or if they didn't, would read the Milner paper we cited). We also thought that the idea of applying it to Prolog was fairly obvious, and that our main contribution was showing that it worked. If someone wants to say that it is not a well-written paper, I'll not gainsay them. But it is one thing to say (for example) that the Mycroft/O'Keefe paper describes the syntax of types and type declaration without spelling out their semantics (a true statement, alas). It is quite another to say in print that you know that the semantics is extralogical! I'm not defending the Mycroft/O'Keefe scheme as being especially wonderful (I repeat that the point of it was to be UNoriginal). My point is to defend it as _logical_. The irony is that, far from being extralogical, the presentation in the paper showed only that the scheme was sound for Horn clauses; we failed to show that it worked for full Prolog. For example, it turns out that cuts can be ignored, but we didn't _prove_ that. Come to that, the Xu and Warren paper doesn't discuss cuts or negation any more than ours did.
jiyang@ecrcvax.UUCP (Jiyang Xu) (10/12/89)
In article <2390@munnari.oz.au>, ok@cs.mu.oz.au (Richard O'Keefe) writes: > I have received other mail from Jiyang Xu and replied to it. > I have not, however, received any mail which clarifies this point. I am sorry I should say I have not received any reply to THAT mail. I received, I think, replies for all my other mails but those addressed to my Stony Brook address (one of them was forwarded by David and I replied based on that). > The point is that you have two related languages, a typed language and > an untyped language. BOTH languages have a semantics; the point of a > type checking theorem is to show that a formula in the typed language > can be evaluated correctly by the untyped interpreter. > In the case of the Mycroft/O'Keefe system, it is again the case that > there are two languages, ***EACH*** with a logical semantics. One of > them is the language with type information in it, call it HCMT (for > Horn Clauses with ML Types). The other is HC (Horn Clauses simpliciter). > The central theorem of the paper is that a program in HCMT can be > interpreted by SLD resolution as an HC program, just by erasing the > types, and that this preserves the semantics of HCMT programs. I never disagree on this point, except I view it in another way: there is one language, the typed language, which should have a logical semantics. By type checking you can optimize away some run-time type checking without affecting the result (or semantics). In the case of M&O system, all such run-time type checking are redundant, if the program is proven "well-typed' by the type checker. So my objection is that your typed language does not have a logical semantics. Let's discuss this again while going through your message. > To repeat, the essence of the idea is that type checking is a compile > time operation whose effect is to reject entire programs, and that the > types have no run-time role at all. "well-typed" programs (in the sense of M&O system) is a subset of all intereting programs that do not need run-time type checkings. > The type system described in the Xu and Warren paper has exactly the > same property! "The type of a predicate [is an] abstract semantics > of the regular program semantics". False. Our regular program semantics _already_ takes in consideration of effects of type declarations. Abstract semantics is just _another_ semantics that makes abstractions and can be viewed as a type language that describes the types of predicates. I wish you have really read the how we define the regular semantics of a program _with_ type declarations (there is a technical error in the version you have read, but at least you should get how the semantics is defined). > If the fact that types play no role at run time is what makes a > type system "extralogical", then the Xu and Warren system is also > extralogical. For the above reason, the assertion is wrong. > Here is what a type declaration looks like in the Mycroft/O'Keefe scheme. > ... (omitted) > Here is the semantics of such a declaration: > ... (omitted) You do not need to tell me these. As I said, this kind of semantics (I term it "first-order logic semantics") is very close to what we had in our earlier work (LP'88 paper) and Lee Naish's work. I wish you had had clarified this in 1984. > It's true that the Mycroft/O'Keefe paper doesn't present exactly this > mapping, but it does say > "Our approach is to consider type specifications as > restrictions on arguments to predicates (and functors). > ... We do not test for violation of such restrictions > at run time, but by statically forbidding all programs > which may lead to a type error. ... the well-typing > rules ... are essentially Horn clauses." I find the last sentence misleading. It took me a while to find where the sentence is --- when talking about implementation of type checker. That is a metaprogram dealing with variable instantiations degrees (less than operation and meta-equality operations) and is meta-logical anyway. > The net effect is that the combination of > - type declarations, > - predicate declarations, and > - Horn clauses > is another set of Horn clauses. The meaning of the declarations and > clauses is defined to be the meaning of the Horn clause program which > results. > > For example, consider the HCMT program > .... I really do not understand why you spend so much time to construct all examples to me. We have written down the very similar thing in our paper and in LP'88 paper (though I am not so sure about the latter) I wonder if you have really gone though the papers. > I repeat, the Xu and Warren type inference system appears to have the > same character: the types which are inferred do not have any run-time > effect. In the main version of the type inference procedure, when there are no type declarations, you are right. When there _are_ type declarations, you may be right and may be wrong, since there is no guarantee that these declarations do not change the semantics, as you pointed out in your append example. We have got another version of TIP that even has run-time effect when there is no type declarations, but have not come up a good theory yet, so I do not want to discuss that yet, though I did include a brief motivation in our paper. Another issue we have not fully addressed is how we can actually enforce the run-time type checking. In M&O system, run-time type checking is needed only for the top level query. > That is, the type checker was not built into DEC-10 Prolog, so although > the type checker could say "this program or query is not well-typed" > (and thus change the semantics of the program or query to "no"), > it could not prevent you running the program in straight DEC-10 Prolog > anyway. Since you seems to believe that type checking is useful only for "debugging" purpose, a type checker is treated as an optional tool just as "dbx", I cannot argue that anymore. If you treat type checker as part of the compiler, as in traditional procedural language, then you cannot make the same claim. Note also since you have included type declarations in your program, how can one run the untransformed program in straight DEC-10 Prolog? You sure have to give a semantics to the program and implement it (discard all the declarations, for instance). > : certain Horn clauses". Are you telling me that > > : p(X1, ..., Xn) :- isa(X1, T1), ..., isa(Xn, Tn), Body. > > : _does not change the semantics of_ > > : p(X1, ..., Xn) :- Body. > > No. I'm saying that it ***DOES*** change the semantics (in a compositional > first-order way), but that for well-typed programs and well-typed queries > you can't DETECT the difference. You do detect the difference because you have to type-check queries at run-time to ensure the well-typedness. > : The point is you did not think this way > > So now he reads minds. Brilliant. It is just because I cannot read your mind so I do not know what your "logical" semantics is. Do not omit the other half of my sentence --- "or you did not claim you think that way". > : How can one tell _which_ semantics you had in mind? > > Reading the paper is a good way. The point is tht Xu CLAIMED TO KNOW > what our semantics was and to know that it was "extralogical". You may well claim that the types in your paper possess an many-sorted logic semantics. Who is going to read your mind? You can even get around the type checker and run the program directly, what can I say to your "semantics" of your type declarations? > Given that the abstract of the paper says explicitly "we observe that > the type resolution problem for a Prolog program is another Prolog > program" it was obvious that we had _some_ sort of logical semantics > in mind. Come on, why do you omit the word "meta" in "... another Prolog (meta) Program". To repeat, your type checker is written in Prolog as a meta program just like an interpreter, which has nothing to do with the semantics of the object program itself (I mean, you can implement any kind of semantics, logical or not). > I did not say that giving a semantics to type declarations is a piece > of cake. Neither did we simply leave it out. The key point, the very > most important thing, about the Mycroft/O'Keefe type system, is that > it is not original. We didn't have to define the semantics of our > polytypes, because we stole them from Milner. The paper was quite > explicit that declarations for predicates were to be viewed as > restrictions on their solution sets. Indeed this is exactly how I understand the semantics of your type checker. However, how to view these restrictions in terms of logic is another issue, which cannot be implied by Milner's paper which talks about typed lambda calculus. The work by Michael Hanus is mostly close to this kind of semantics and to that in M&O paper as I understand, but the semantics you are claim now is NOT obviously related to Milner's work. > Re-reading the Mycroft & O'Keefe paper, I have to agree that it doesn't > spell things out much. Unfortunately, both of us were PhD students who > were supposed to be doing other things, and we thought that everyone > understood the ML type system (or if they didn't, would read the Milner > paper we cited). We also thought that the idea of applying it to Prolog > was fairly obvious, and that our main contribution was showing that it > worked. If someone wants to say that it is not a well-written paper, > I'll not gainsay them. But it is one thing to say (for example) that > the Mycroft/O'Keefe paper describes the syntax of types and type > declaration without spelling out their semantics (a true statement, alas). > It is quite another to say in print that you know that the semantics is > extralogical! Still, from your way of presenting it, may not be the way you thought about it, one can only get the conclusion that the semantics is extra-logical. Also, giving the following program and type declarations: type color => red, green, blue. type mycolor => red, green, blue. pred p(color). pred q(mycolor). clause p(X) :- q(X). will your type checker fail to well-type it? If you change the declation to "pred q(color)", the semantics as you claimed remains the same, but now the program is well-typed. Of course this example is meaningless but the name equivalence and strutural equivalence in Pascal types have been disputed along this line. Also, I do not claim we solve all the problem which is unlikely if we allow arbitrary type definitions. Nobody's doubted the quality of your paper. All later work cites your paper. There are so many papers in this area but we take yours as the representative one. The point is that paper was written in 1984, we (include you) have learned a lot since then, a large part from your paper. Why cannot the work be improved? If I did not consider that's a good paper, I would not compare ours with it, would not even cite it. You do not blame our ancestor for not knowing how to add 4 to 7, do you. I was also a Ph.D. student (and theoretically I still am), how could I understand that a single assertion that you think is wrong makes you so angry. -- Jiyang