🚀 go-pugleaf

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.