Path: utzoo!attcan!utgpu!jarvis.csri.toronto.edu!mailrus!cs.utexas.edu!uunet!mcsun!unido!ecrcvax!jiyang
From: jiyang@ecrcvax.UUCP (Jiyang Xu)
Newsgroups: comp.lang.prolog
Subject: Re: What does "extralogical" mean?
Summary: Prolog, type checking
Keywords: usage
Message-ID: <787@ecrcvax.UUCP>
Date: 12 Oct 89 13:28:04 GMT
References: <2204@munnari.oz.au> <786@ecrcvax.UUCP> <2390@munnari.oz.au>
Organization: ECRC, Munich 81, West Germany
Lines: 228

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