Types
Jim Bowery
While it is true that types started out as pragmatic means of checking
program consistency and generating optimized code at compile time, the
recent explosion of interest in abstract types has shifted the emphasis
quite a bit toward the advantages to be gained by polymorphism, which is
just a fancy way of saying "make the name of the operation have a
consistent meaning regardless of what sort of thing it is operating on."
This is where we start to push type inference beyond simple label
checking and, finally, to inferential programming itself -- and even the
documentation value of type declarations starts to dissolve.
People who have worked with OO since the days of Smalltalk '80 have come
to realize that the best OO design maximizes polymorphism by constructing
the most parsimonious "theory" to describe the program or set of programs
being written. Such parsimony leads directly to difficulty in achieving
compile-time type inference and, as I've already tried to point out, begs
for an inferential language in which to express the program itself.
Pragmatically speaking, there are lots of extra-language directives one
can hand the compiler/interpreter to help it do its job, but if one abuses
such directives by overuse, one is led into sloppy design practice (which,
I will admit, is usually a pragmatic reality one has to deal with).
So pragmas are a necessary adjunct to any pragmatic language, but the
real question is, must they be part of the language itself?
--
The promotion of politics exterminates apolitical genes in the population.
The promotion of frontiers gives apolitical genes a route to survival.
Change the tools and you change the rules.
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>While it is true that types started out as pragmatic means of checking
>program consistency and generating optimized code at compile time, the
>recent explosion of interest in abstract types has shifted the emphasis
>quite a bit toward the advantages to be gained by polymorphism, which is
>just a fancy way of saying "make the name of the operation have a
>consistent meaning regardless of what sort of thing it is operating on."
Indeed, there _has_ been an explosion of interest in this area, and
we have seen a lot of progress... things like Haskell-style type classes and
existential types can be extremely expressive.
>This is where we start to push type inference beyond simple label
>checking
Agreed.
>and, finally, to inferential programming itself --
This claim is a bit more controversial.
What do you mean by "inferential programming"?
>and even the documentation value of type declarations starts to dissolve.
This claim I find mystifying.
>People who have worked with OO since the days of Smalltalk '80 have come
>to realize that the best OO design maximizes polymorphism by constructing
>the most parsimonious "theory" to describe the program or set of programs
>being written. Such parsimony leads directly to difficulty in achieving
>compile-time type inference
... which suggests (to me) that perhaps we should be declaring the types,
rather than trying to get the compiler to infer them -- at least for the
difficult cases. For one thing, if a compiler has trouble inferring the
types, then there is a good chance that a human reader may have trouble too...
>and, as I've already tried to point out, begs
>for an inferential language in which to express the program itself.
I'm still not sure what you mean by an inferential language.
It sounds a little bit like you are trying to suggest that
when we "push type inference beyond simple label checking",
then we will end up with somethiing like Prolog. But that
seems pretty unlikely to me, so maybe I have misunderstood
what you were trying to say.
>Pragmatically speaking, there are lots of extra-language directives one
>can hand the compiler/interpreter to help it do its job,
I think you misunderstand the role of types in logic programming.
Typically types are not there just to help the compiler do its job,
but rather they are an integral part of the specification.
I can discuss this in more detail if you wish, but several researchers
have already addressed this topic in much more detail than I can do in
a news posting. See for example Lee Naish's work that I previously
cited, and also Yves Deville's book [*].
[*] I forget the exact title, but I think the title contains the phrases
"Logic programming" and "systematic design".
>but if one abuses
>such directives by overuse, one is led into sloppy design practice (which,
>I will admit, is usually a pragmatic reality one has to deal with).
The implication here seems to be that if you use explicit type declarations,
then you will be led into "sloppy design practice".
All I can say here is that this contradicts my experience.
My experience is that
(1) one of the most important factors in avoiding sloppy
design is making sure that you _write the design down_;
(2) types are usually a very important part of the design;
(3) type declarations are a good way of writing down the
part of the design that deal with types.
--
Fergus Henderson <f...@cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger f...@128.250.37.3 | -- the last words of T. S. Garp.
Jim Bowery
Jim Bowery (jabo...@netcom.com) wrote:
: ..."permissible" ultimately
: expresses itself in a logical failure to meet certain conditions.
^^^^^^^
make that success
Logic inversion after a long bike ride...
Jim Bowery
Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
: jabo...@netcom.com (Jim Bowery) writes:
: >and even the documentation value of type declarations starts to dissolve.
: This claim I find mystifying.
If the shift toward polymorphism is well motivated, then it becomes
less desirable to state what type of object an operation is being
performed on since that impacts reuse and, indeed, the very nature
of abstraction as defined by the set of permitted operations as opposed
to the set of permitted values.
: >People who have worked with OO since the days of Smalltalk '80 have come
: >to realize that the best OO design maximizes polymorphism by constructing
: >the most parsimonious "theory" to describe the program or set of programs
: >being written. Such parsimony leads directly to difficulty in achieving
: >compile-time type inference
: ... which suggests (to me) that perhaps we should be declaring the types,
: rather than trying to get the compiler to infer them --
But the reason you wanted the compiler to infer them in the first place is
because the human was having trouble keeping the polymorphism clean! I
think that we have an "impedence mismatch" around here somewhere ;-).
: It sounds a little bit like you are trying to suggest that
: when we "push type inference beyond simple label checking",
: then we will end up with somethiing like Prolog. But that
: seems pretty unlikely to me, so maybe I have misunderstood
: what you were trying to say.
No, that is exactly what I'm saying. I really think people aren't
taking seriously enough the idea that abstract data types are defined
by the set of permissible operations -- and "permissible" ultimately
expresses itself in a logical failure to meet certain conditions.
I appreciate your references but its not like I haven't been aware of
languages like Haskell since the early 80's (and even got Curry's autograph
to prove it ;-).
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>
>: jabo...@netcom.com (Jim Bowery) writes:
>
>: >and even the documentation value of type declarations starts to dissolve.
>
>: This claim I find mystifying.
>
>If the shift toward polymorphism is well motivated,
I agree that it is.
>then it becomes
>less desirable to state what type of object an operation is being
>performed on since that impacts reuse and, indeed, the very nature
>of abstraction as defined by the set of permitted operations as opposed
>to the set of permitted values.
Ah, now I understand. But I don't agree with your conclusion.
You're right that we want to avoid stating what the particular
concrete types of the objects involved. However, that doesn't
mean we should stop documenting the types entirely -- it is still
important to document our designs, even if they are more abstract.
(In fact perhaps _particularly_ if they are more abstract.)
We should document for each object what set of permitted operations
we are assuming; or equivalently, we should document what class
of types are allowed for each object (where a class is defined
by the set of permitted operations).
I think our difference in philosophies here is the difference
between accidental reuse and deliberate reuse. You want the
implementor of a procedure to implement it and then have the
users of the procedure be able to use it in whichever ways
will happen to work. I want the implementor to carefully decide
how reusable they intend the procedure to be, and then only allow
users to reuse it in the intended ways. (They can go back and
reconsider their decision, of course; but it must be an deliberate
decision.)
Accidental reuse is fundamentally flawed, IMHO; it introduces undesirable
coupling that can lead to "OO spaghetti". It can be good for rapid
protyping, but it is awful for maintenance. The basic problem is that
if someone has reused my procedure in ways that I didn't intend, then I
am no longer free to change its implementation, because by doing so I
might break that other person's code.
Peter Gabriel talks about this in his book "Patterns of Software";
he uses the term "unnecessary compression". Reuse is not _invariably_
a good thing; there are good forms of reuse and bad ones.
>: >People who have worked with OO since the days of Smalltalk '80 have come
>: >to realize that the best OO design maximizes polymorphism by constructing
>: >the most parsimonious "theory" to describe the program or set of programs
>: >being written. Such parsimony leads directly to difficulty in achieving
>: >compile-time type inference
>
>: ... which suggests (to me) that perhaps we should be declaring the types,
>: rather than trying to get the compiler to infer them --
>
>But the reason you wanted the compiler to infer them in the first place is
>because the human was having trouble keeping the polymorphism clean!
I didn't want them for that reason. The only reason I wanted them
was to save typing, and to reduce unnecessary clutter. But I consider
it crucial to explicitly document my interfaces.
>: It sounds a little bit like you are trying to suggest that
>: when we "push type inference beyond simple label checking",
>: then we will end up with somethiing like Prolog. But that
>: seems pretty unlikely to me, so maybe I have misunderstood
>: what you were trying to say.
>
>No, that is exactly what I'm saying.
In that case, I'm going back to my original reply at the start of this
thread: types provide three main benefits (documentation, compile-time
error checking, and efficiency), and none of these are present in Prolog.
I should in fact mention another important benefit, and this is also not
present in Prolog: OOP-style (or Haskell typeclass-style) polymorphism.
You don't need static types for this, dynamic types will work fine too,
if they have operations attached -- but Prolog doesn't have that.
In Prolog, if you want to do this, then you have to explicitly pass
the types around.
IMHO, any type system that attempts to "push type inference beyond simple
label checking" must still retain these four benefits. So I can't
imagine the result being similar to Prolog.
Jim Bowery
Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
: Ah, now I understand. But I don't agree with your conclusion.
: You're right that we want to avoid stating what the particular
: concrete types of the objects involved. However, that doesn't
: mean we should stop documenting the types entirely --
I agree -- but I think we differ on how one documents those types.
I would include them in an extra-language syntax ala pragmas that
do not impact the formal meaning of the program -- they merely
provide clues to the compiler/interpreter and the maintainer -- and they
could be easily added/removed/modified without altering other source.
: it is still
: important to document our designs, even if they are more abstract.
I agree.
: (In fact perhaps _particularly_ if they are more abstract.)
I don't agree. As we achieve greater abstract expression, we
achieve greater unity with specification. Beyond that all is prose.
: We should document for each object what set of permitted operations
: we are assuming; or equivalently, we should document what class
: of types are allowed for each object (where a class is defined
: by the set of permitted operations).
I think you should take a look at the language "Self" from Sunsoft
sometime (not urgent). Basically, they get rid of classes by allowing
you to use any existing object as a template for a new object. This,
of course, implies the inheritance of various capabilities/properties.
: I think our difference in philosophies here is the difference
: between accidental reuse and deliberate reuse.
Terse theories can exhibit the qualities of Ockham's Razor
(generalizations that work) but they can also exhibit the properties of
Ockham's Chainsaw Massacre (generalizations that don't work).
Where we differ is in how one achieves the former rather than the latter.
IMHO, this is more a property of the quality of the theory than any formal
baggage we hang around the theoretician's neck. Having said that, I agree
that good theoreticians are in short supply and their time is in demand.
As Mark Twain once wrote (paraphrased) "I apologize for not having the
time to make this shorter." Basically, that means programming is largely
the technology of making bad theories work well enough to make money. I
don't object to encumbering the programmer (we won't glorify him as a
theoretician any longer here) as long as it is done in a way that doesn't
get in the way of additional investments yielding the clean theoretic
structure we all (I'm presuming to speak for you here) desire. In the
end, Ockham's Razor is the proper goal.
: You want the
: implementor of a procedure to implement it and then have the
: users of the procedure be able to use it in whichever ways
: will happen to work. I want the implementor to carefully decide
: how reusable they intend the procedure to be, and then only allow
: users to reuse it in the intended ways. (They can go back and
: reconsider their decision, of course; but it must be an deliberate
: decision.)
Seymour Cray once said that the difference between good engineers and
great engineers is that great engineers figure out ways of using tools
that their inventors never imagined. What Cray didn't say, which he
should have, was that the difference between good tool-makers and great
tool-makers is that when great engineers do their thing with his tools,
they don't get themselves into trouble.
This is a matter of quality. If the abstraction is clear and clean,
relying on it during the creative act won't get you into trouble.
This may be getter all too philosophical for this newsgroup, but I really
think it is important in the decision of how one imposes pragmatics on a
programming language syntax.
: Accidental reuse is fundamentally flawed, IMHO; it introduces undesirable
: coupling that can lead to "OO spaghetti". It can be good for rapid
: protyping, but it is awful for maintenance. The basic problem is that
: if someone has reused my procedure in ways that I didn't intend, then I
: am no longer free to change its implementation, because by doing so I
: might break that other person's code.
I don't hve a problem with the tool-maker placing warning labels on his
tools. I just think it should be easy to remove the labels.
: Peter Gabriel talks about this in his book "Patterns of Software";
: he uses the term "unnecessary compression". Reuse is not _invariably_
: a good thing; there are good forms of reuse and bad ones.
Yes. There is Ockham's Razor and Ockham's Chainsaw Massacre.
: >: It sounds a little bit like you are trying to suggest that
: >: when we "push type inference beyond simple label checking",
: >: then we will end up with somethiing like Prolog. But that
: >: seems pretty unlikely to me, so maybe I have misunderstood
: >: what you were trying to say.
: >
: >No, that is exactly what I'm saying.
: In that case, I'm going back to my original reply at the start of this
: thread: types provide three main benefits (documentation, compile-time
: error checking, and efficiency), and none of these are present in Prolog.
Yes. Prolog is inadequate. But was was responding to the phrase
"something like Prolog", which I interpret differently than you.
: IMHO, any type system that attempts to "push type inference beyond simple
: label checking" must still retain these four benefits. So I can't
: imagine the result being similar to Prolog.
I'll see if I can work up some believable examples and get back to you.
Perhaps you are correct that it won't be "similar to Prolog" but that is
a matter of perception.
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>
>: You're right that we want to avoid stating what the particular
>: concrete types of the objects involved. However, that doesn't
>: mean we should stop documenting the types entirely --
>
>I agree -- but I think we differ on how one documents those types.
>I would include them in an extra-language syntax ala pragmas that
>do not impact the formal meaning of the program -- they merely
>provide clues to the compiler/interpreter and the maintainer -- and they
>could be easily added/removed/modified without altering other source.
A had a similar view, until Lee Naish converted me ;-)
Basically the issue is this: if your specification calls for
a predicate that appends lists, do you write
append([], Xs, Xs).
append([X|Xs], Ys, [X|Zs]) :- append(Xs, Ys, Zs).
or do you write
append([], Xs, Xs) :- is_list(Xs).
append([X|Xs], Ys, [X|Zs]) :- append(Xs, Ys, Zs).
is_list([]).
is_list([_|Xs]) :- is_list(Xs).
?
If you write the former, then it is not correct with respect to the
specification unless types are a part of the semantics.
Making types part of the semantics may have disadvantages, but it seems
to me to be not nearly as bad as either of the immediately obvious
alternatives -- explicitly insert calls such as `is_list' into the
program, or writing programs that are not correct with respect to their
specifications.
>Terse theories can exhibit the qualities of Ockham's Razor
>(generalizations that work) but they can also exhibit the properties of
>Ockham's Chainsaw Massacre (generalizations that don't work).
Nice terminology ;-)
Fergus Henderson
I wrote:
>A had a similar view, until Lee Naish converted me ;-)
Sorry, that should be "I had a similar view...".
^
KMorris692
In article <6025jg$4...@mulga.cs.mu.OZ.AU>, f...@mundook.cs.mu.OZ.AU (Fergus
Henderson) writes:
>Basically the issue is this: if your specification calls for
>a predicate that appends lists, do you write
>
> append([], Xs, Xs).
> append([X|Xs], Ys, [X|Zs]) :- append(Xs, Ys, Zs).
>
>or do you write
>
> append([], Xs, Xs) :- is_list(Xs).
> append([X|Xs], Ys, [X|Zs]) :- append(Xs, Ys, Zs).
>
> is_list([]).
> is_list([_|Xs]) :- is_list(Xs).
>
>?
>
>If you write the former, then it is not correct with respect to the
>specification unless types are a part of the semantics.
It's worse than that. Guess what happens if you use the latter with the
2nd argument unbound? You get premature binding.
?- append([1,2,3],T,L).
T=[], L=[1,2,3];
T=[V1|V2], L=[1,2,3,V1|V2];
T=[V1,V2|V3], L=[1,2,3,V1,V2|V3];
...
----
"Communication is possible only between equals." -- Hagbard Celine
Karen A. Morrissey
KMorr...@aol.com
303-753-2968
Jim Bowery
Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
: I had a similar view, until Lee Naish converted me ;-)
Well, I'm still testing type-negative so Naish must not have converted me
yet.
This whole thing about lists and their pattern matching is a
bastardization of the predicate calculus that I would say fits under the
"poor quality tool" heading.
To see what I mean, try reformulating Naish's mental retrovirus with the
following formalism and see where it leads you:
append(X,Y,Z) :- head(Z,X),tail(Z,Y).
Jim Bowery
(Elaboration of a previous post which hopefully was deleted.)
Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
: I had a similar view, until Lee Naish converted me ;-)
Well, I'm still testing type-negative so Naish must not have converted me
yet.
This whole thing about lists and their pattern matching is a
bastardization of the predicate calculus that I would say fits under the
"poor quality tool" heading.
To see what I mean, try reformulating Naish's mental retrovirus (along
with lists themselves) with the following formalism and see where it leads
you:
append([],Xs,Xs) :- is_list(Xs).
append(XXs,Ys,XZs):-
head(XXs,X),tail(XXs,Xs),
head(XZs,X),tail(XZs,Zs),
append(Xs,Ys,Zs).
is_list([]).
is_list(NXs) :- head(NXs,N),tail(NXs,Xs),is_list(Xs).
When I cease to think of "head" and "tail" as somehow special -- but
merely as predicates along with the rest of the universe's predicates,
Naish's dilemma is actually a problem with _any_ inference where there is
partial success -- and this is routinely the case. It is simply not
possible nor desirable to guarantee successful unification through typing.
HOWEVER, having said that, this is a pretty good example of what I mean
about using Prolog as a type specification language.
If we add a pragma that tells the compiler/maintainer that the predicate
"is_list" is a type specification -- or better yet, that it is something
that must be verified at compile time, we have started down a healthier
path.
Lee Naish
In article <jaboweryE...@netcom.com>, jabo...@netcom.com (Jim Bowery) writes:
>
> Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
> : I had a similar view, until Lee Naish converted me ;-)
>
> Well, I'm still testing type-negative so Naish must not have converted me
> yet.
> To see what I mean, try reformulating Naish's mental retrovirus (along
> with lists themselves) with the following formalism and see where it leads
> you:
Well, I for one can't follow what this posting has to do with my work.
Perhaps its that mental retrovirus I have :-) For those of daring spirit
(or a strong immune system), take a look at
@incollection{naish:90,
author = {Naish, Lee},
title = {Types and the intended meaning of logic programs},
pages = {189-216},
booktitle = {Types in logic programming},
editor = {Frank Pfenning},
publisher = {MIT Press},
address = {Cambridge, Massachusetts},
year = {1992},
comment = {Technical Report 90/4, Department of Computer
Science, University of Melbourne}
}
lee
Jim Bowery
Lee Naish (l...@cs.mu.OZ.AU) wrote:
: Well, I for one can't follow what this posting has to do with my work.
: Perhaps its that mental retrovirus I have :-) For those of daring spirit
: @incollection{naish:90,
: author = {Naish, Lee},
Thanks for the plug, but what's the going rate for your innoculation? :-)
Anyway, the response string is bringing up interesting issues regardless
of its relevance to your work, so I hope your epiphany here won't inhibit
further discourse.
Jim Bowery
As it happens, I got to pass by Palo Alto today, so being careful to avoid
the hillbilly girl and her Men In Black, I stole into the Stanford CS
library and grabbed a copy of Naish's paper. It's got quite a bit to do
with this response string, as a matter of fact, but will take a while to
read on its own terms, which are rather turgid in a few places. For
example when he gives the possible intended interpretations/specifications
of append:
"1. If A, B and C are lists then C is B concatenated onto A. This implies
that if append is called with the first two arguments lists, any non-list
can be returned as the third argument."
This just doesn't make sense to me, and it isn't the only such sentence.
Also, I don't get what the motive is for removing the type predicates
from the actual program and placing them in separate type declarations:
append(A,B,C) type list(A), list(B), list(C).
append([],A,A).
append(A.B, C, A.D) :- append (B,C,D).
where
list([]).
list(H.T) :- list(T).
It seems the compiler should be able to infer the type declaration from:
append([],A,A) :- list(A).
with, perhaps, a pragma declaring "list" to be a type predicate if that
can't be inferred by the compiler as well.
In any case, Naish looks like he is in the general ballpark of at least
using the generalized inference engine of Prolog to do some compile-time
type inference.
Is this implemented anywhere?
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>For example when he [Naish] gives the possible intended
>interpretations/specifications of append:
>
>"1. If A, B and C are lists then C is B concatenated onto A. This implies
>that if append is called with the first two arguments lists, any non-list
>can be returned as the third argument."
>
>This just doesn't make sense to me, and it isn't the only such sentence.
Hmm, it makes perfect sense to me.
Perhaps if I translate the first sentence to predicate calculus?
Specification:
append(A, B, C) <=>
(list(A) /\ list(B) /\ list(C) =>
'x is y concatenated onto z'(C, B, A)).
From this specification you can deduce that
list(A) /\ list(B) /\ not(list(C)) => append(A, B, C)
which explains his second sentence.
>Also, I don't get what the motive is for removing the type predicates
>from the actual program and placing them in separate type declarations:
...
>It seems the compiler should be able to infer the type declaration from:
>
>append([],A,A) :- list(A).
>
>with, perhaps, a pragma declaring "list" to be a type predicate if that
>can't be inferred by the compiler as well.
The motivation, as I see it, is this:
1. Clarity.
From a specification point of view, a procedure should not
be required to ensure the type-correctness of arguments that
it does not bind -- that should be the compiler's responsibility
(for "regular" types, e.g. list) and/or the caller's responsibility
(for "irregular" types, e.g. sorted_list).
Hence, when the time comes to actually implement a specification,
it is important to distinguish between the types and other parts
of the specification.
It is also useful for a programmer to know which parts are the
regular types, because the programmer can be sure that the
consistency of those types has been checked by the compiler,
whereas checking the consistency of irregular types has to be
done by the programmer.
2. Brevity.
Using a separate notation for types allows programs to be more
concise, particularly if you let the compiler infer the
regular parts of the types.
>In any case, Naish looks like he is in the general ballpark of at least
>using the generalized inference engine of Prolog to do some compile-time
>type inference.
>
>Is this implemented anywhere?
Yes, the NU-Prolog type checker has support for the stuff described in
Naish's paper.
However, I must say that in practice I found it less useful than
the Mercury type checker. In fact I began developing the type checker
which later became the Mercury type checker precisely because I found
the NU-Prolog type checker to be inadequate. The problem was that
the NU-Prolog type checker was too lax. One problem was that it basically
only reported an error when it could prove that a clause was type-incorrect,
rather than when it couldn't prove that a clause wasn't type-incorrect.
In practice I found that it would often fail to report anything even
though the program it was checking contained type errors.
Robert F. Staerk
In article <5vtlt9$e...@mulga.cs.mu.OZ.AU>, f...@mundook.cs.mu.OZ.AU (Fergus
Henderson) wrote:
> In that case, I'm going back to my original reply at the start of this
> thread: types provide three main benefits (documentation, compile-time
> error checking, and efficiency), and none of these are present in Prolog.
One can argue that type correctness is like any other program property
and can be established by means of a proof rather than by syntactic
restraints. As an example I include some properties of append that have
been proved using LPTP (an interactive Logic Program Theorem Prover).
Note that, for example, the uniqueness of append in the first argument
is not so trivial to establish.
The following predicates are used:
list([]).
list([X|L]) :- list(L).
append([],L,L).
append([X|L1],L2,[X|L3]) :- append(L1,L2,L3).
See also: http://www2-iiuf.unifr.ch/tcs/robert.staerk/lptp/list.html
----------------------------------------------------------------------------
Lemma (append:types:1)
all [l1,l2,l3]: succeeds append(?l1,?l2,?l3) => succeeds list(?l1).
Lemma (append:types:2)
all [l1,l2,l3]: succeeds append(?l1,?l2,?l3) & succeeds list(?l2) =>
succeeds list(?l3).
Lemma (append:types:3)
all [l1,l2,l3]: succeeds append(?l1,?l2,?l3) & succeeds list(?l3) =>
succeeds list(?l2).
Lemma (append:termination:1)
all [l1,l2,l3]: succeeds list(?l1) => terminates append(?l1,?l2,?l3).
Lemma (append:termination:2)
all [l1,l2,l3]: succeeds list(?l3) => terminates append(?l1,?l2,?l3).
Lemma (append:existence)
all [l1,l2]: succeeds list(?l1) => (ex l3: succeeds append(?l1,?l2,?l3)).
Lemma (append:uniqueness)
all [l1,l2,l3,l4]: succeeds append(?l1,?l2,?l3) &
succeeds append(?l1,?l2,?l4) => ?l3 = ?l4.
Definition (**/2)
all [l1,l2,l3]: succeeds list(?l1) =>
(?l1 ** ?l2 = ?l3 <=> succeeds append(?l1,?l2,?l3)).
Theorem (app:associative)
all [l1,l2,l3]: succeeds list(?l1) & succeeds list(?l2) =>
(?l1 ** ?l2) ** ?l3 = ?l1 ** (?l2 ** ?l3).
Theorem (app:lh)
all [l1,l2]: succeeds list(?l1) & succeeds list(?l2) =>
lh(?l1 ** ?l2) = lh(?l1) @+ lh(?l2).
Lemma (append:uniqueness:1)
all [l1,l2,l3,l4]: succeeds append(?l1,?l2,?l3) &
succeeds append(?l4,?l2,?l3) & succeeds list(?l3) => ?l1 = ?l4.
Lemma (append:uniqueness:2)
all [l1,l2,l3,l4]: succeeds append(?l1,?l2,?l3) &
succeeds append(?l1,?l4,?l3) => ?l2 = ?l4.
----------------------------------------------------------------------------
--
Robert F. Staerk http://www-iiuf.unifr.ch/~staerk
Institute of Informatics robert...@unifr.ch
University of Fribourg
Rue Faucigny 2
CH-1700 Fribourg, Switzerland
Jim Bowery
: ...
: >It seems the compiler should be able to infer the type declaration from:
: >
: >append([],A,A) :- list(A).
: >
: >with, perhaps, a pragma declaring "list" to be a type predicate if that
: >can't be inferred by the compiler as well.
: The motivation, as I see it, is this:
: 1. Clarity.
It's hard to see what could be clearer than the specification itself.
: From a specification point of view, a procedure should not
: be required to ensure the type-correctness of arguments that
: it does not bind
What procedure? This?: append([],A,A) :- list(A).
What specification? This?: append([],A,A) :- list(A).
It seems that this specification/procedure should suffice as the
actual program and the PROGRAMMER should not be required to
perform any further transformations.
: -- that should be the compiler's responsibility
Exactly my point. Whence comes this terror of execution time overhead of
type checking (eg: ":- list(A).") when the optimizer would simply
eliminate that code from the execution binary anyway? Its sole purpose is
to provide type information for compile time type inference. In cases
where inference cannot be accomplished at compile time it seems the type
checking is indistinguishable from normal logical evaluation and must be
performed at execution time anyway, just like any other aspect of the
program that can't be optimized out at compile time.
: It is also useful for a programmer to know which parts are the
: regular types, because the programmer can be sure that the
: consistency of those types has been checked by the compiler,
: whereas checking the consistency of irregular types has to be
: done by the programmer.
It seems the "regular types" are simply those that are checked as part of
the specification and "irregular types" are simply those that are checked
as part of the USE of the specified logic. Why not leave it at that and
let the compiler figure out what code to generate, with, perhaps, a little
human guidance in the form of pragmas?
KMorris692
In article <60879o$i...@mulga.cs.mu.OZ.AU>, f...@mundook.cs.mu.OZ.AU (Fergus
Henderson) writes:
>jabo...@netcom.com (Jim Bowery) writes:
> [...]
>>"1. If A, B and C are lists then C is B concatenated onto A. This implies
>>that if append is called with the first two arguments lists, any non-list
>>can be returned as the third argument."
>>
>>This just doesn't make sense to me, and it isn't the only such sentence.
>
>Hmm, it makes perfect sense to me.
>
>Perhaps if I translate the first sentence to predicate calculus?
>
>Specification:
> append(A, B, C) <=>
> (list(A) /\ list(B) /\ list(C) =>
> 'x is y concatenated onto z'(C, B, A)).
>
>From this specification you can deduce that
>
> list(A) /\ list(B) /\ not(list(C)) => append(A, B, C)
>
>which explains his second sentence.
I'm being slow-witted today -- too many positive ions, I suspect :-) --
and I don't recall the meanings of <=> and => . Would you briefly name
those operators and/or the rule of deduction you used?
Jim Bowery
Robert F. Staerk (robert...@unifr.ch) wrote:
: One can argue that type correctness is like any other program property
: and can be established by means of a proof rather than by syntactic
: restraints. As an example I include some properties of append that have
: been proved using LPTP (an interactive Logic Program Theorem Prover).
Such powerful tools should be routinely included in compilers not only for
type correctness checking, but for optimization -- which seems to be a
major motive in all these "type" systems. The "interactive" aspect
should basically consist of the pragmas provided by the human.
Thomas Charles CONWAY
jabo...@netcom.com (Jim Bowery) writes:
>Robert F. Staerk (robert...@unifr.ch) wrote:
>: One can argue that type correctness is like any other program property
>: and can be established by means of a proof rather than by syntactic
>: restraints. As an example I include some properties of append that have
>: been proved using LPTP (an interactive Logic Program Theorem Prover).
>
>Such powerful tools should be routinely included in compilers not only for
>type correctness checking, but for optimization -- which seems to be a
>major motive in all these "type" systems. The "interactive" aspect
>should basically consist of the pragmas provided by the human.
Although the Mercury implementation makes use of the fact that programs
must be well typed, the major motivation for the use of a type system
is for helping programmers to write correct programs.
Thomas
--
ZZ:wq!
^X^C
Thomas Conway con...@cs.mu.oz.au
AD DEUM ET VINUM Every sword has two edges.
Tyson Richard DOWD
jabo...@netcom.com (Jim Bowery) writes:
>: 1. Clarity.
This seriously undermines the confidence I have in my program,
because I know that a certainly class of errors (type errors)
may still be present in the program, waiting to be triggered by
execution flow or input data. Static checking has the advantage
that you can be sure these errors are eliminated before runtime.
The cases where type inference cannot be accomplished at compile time
that you talk about are almost always errors in my code. I would
prefer to have static checking tell me it cannot prove them correct,
than have the compiler silently produce inefficient code that will
check - either succeeding and wasting cycles, or blurt out "type error,
exiting" at runtime.
If I want the choice between these two extremes, I'd prefer to be able
to control it with user level dynamic types.
>: It is also useful for a programmer to know which parts are the
>: regular types, because the programmer can be sure that the
>: consistency of those types has been checked by the compiler,
>: whereas checking the consistency of irregular types has to be
>: done by the programmer.
>It seems the "regular types" are simply those that are checked as part of
>the specification and "irregular types" are simply those that are checked
>as part of the USE of the specified logic. Why not leave it at that and
>let the compiler figure out what code to generate, with, perhaps, a little
>human guidance in the form of pragmas?
If regular types are checked as part of the specification, what harm
is there in letting the compiler check them again? And for those without
a specification, or making modifications to an unspecified program,
the checks can only be helpful.
I can understand the desire to put better language support for irregular
type checking in, optimized where possible, but I can't see how this
would make you want to decrease the amount of static checking done.
There is a line I would like to draw for the compiler, that says -
"don't even compile it if you can't prove at least this much".
I'd like this because it increases my confidence in the code, and it
gives me a baseline from which I know the system can produce reasonably
efficient code.
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>: jabo...@netcom.com (Jim Bowery) writes:
>: >Also, I don't get what the motive is for removing the type predicates
>: >from the actual program and placing them in separate type declarations:
>
>: The motivation, as I see it, is this:
>
>: 1. Clarity.
>
>It's hard to see what could be clearer than the specification itself.
Clearer than the formal specification?
I don't know about you, but I certainly find English a lot easier to
read than predicate calculus. I'm pretty sure I'm not alone in this.
Formal specifications are _precise_, but not necessarily easy to understand.
Code is written by humans, and it needs to be understandable by humans.
Having a single uniform notation for everything is not necessarily a good
way of achieving this. (Try zeros and ones... very uniform ;-)
There is a fine line between on the one hand _unifying_ two related concepts,
and on the other hand _confusing_ two related concepts.
For example, "classes" in OOP languages like C++ or Java unify the two concepts
of "module" and "type" in languages like Ada or Haskell... or do they
just confuse them? It's a difficult issue.
If the different parts of a specification serve different purposes,
or need to be given different emphasis at different times during the
software development process, then it is probably best to use different
notation for them. That way it is easy to tell them apart!
Sure, a compiler can do lots of nifty analysis, but it shouldn't be
necessary for a human reader to do global analysis of a program in
order to understand it.
>: From a specification point of view, a procedure should not
>: be required to ensure the type-correctness of arguments that
>: it does not bind
>
>What procedure? This?: append([],A,A) :- list(A).
>
>What specification? This?: append([],A,A) :- list(A).
>
>It seems that this specification/procedure should suffice as the
>actual program and the PROGRAMMER should not be required to
>perform any further transformations.
That only works for regular types. For irregular types,
in general compilers won't be able to infer them;
and yet sometimes it would be much too expensive to check them.
In those cases, you need to leave the checks out of the procedure.
But you should not modify the specification.
>: -- that should be the compiler's responsibility
>
>Exactly my point.
You elided "... or the caller's responsibility", which was an important
part of my point. It can't be just the compiler's responsibility.
>Whence comes this terror of execution time overhead of
>type checking (eg: ":- list(A).") when the optimizer would simply
>eliminate that code from the execution binary anyway? Its sole purpose is
>to provide type information for compile time type inference.
That's not what I'm worried about.
I'm worried about two things:
- the execution time overhead of checking non-regular types
(the sort that compilers can't verify)
- the effect on readability of the code.
>In cases
>where inference cannot be accomplished at compile time it seems the type
>checking is indistinguishable from normal logical evaluation and must be
>performed at execution time anyway, just like any other aspect of the
>program that can't be optimized out at compile time.
No, not at all. For the irregular parts of types, the _programmer_ is
the one doing the proof of type-correctness. Those parts of the
logic are evaluated not at run time, nor even at compile time, but
rather at coding time.
Sometimes it is helpful to check them at runtime also, just to double-check
the programmer's proof (since most programmers are pretty sloppy when
it comes to proofs). But often that is infeasible.
Naish gives an example of an irregular type which is undecidable.
Fergus Henderson
kmorr...@aol.com (KMorris692) writes:
>f...@mundook.cs.mu.OZ.AU (Fergus Henderson) writes:
>
>>Perhaps if I translate the first sentence to predicate calculus?
>>
>>Specification:
>> append(A, B, C) <=>
>> (list(A) /\ list(B) /\ list(C) =>
>> 'x is y concatenated onto z'(C, B, A)).
>>
>>From this specification you can deduce that
>>
>> list(A) /\ list(B) /\ not(list(C)) => append(A, B, C)
>>
>>which explains his second sentence.
>
>I'm being slow-witted today -- too many positive ions, I suspect :-) --
>and I don't recall the meanings of <=> and => . Would you briefly name
>those operators and/or the rule of deduction you used?
<=> means "if and only if". X Y X<=>Y X=>Y X/\Y
=> means "implies". t t t t t
/\ means "and". t f f f f
Also \/ means "or". f t f t f
See table on right: f f t t f
The deduction goes
append(A, B, C) <= (list(A) /\ list(B) /\ list(C) => p(C, B, A))
[hypothesis]
<= not((list(A)) /\ list(B) /\ list(C)) \/ p(C,B,A)
[because X => Y === not(X) \/ Y]
<= not((list(A)) /\ list(B) /\ list(C))
[because X => X \/ Y]
<= (list(A)) /\ list(B) /\ not(list(C)))
[because X /\ not(Y) => not(X /\ Y)]
I suppose this is a bit counter-intuitive, but I think that is Naish's
point -- this is a bad choice for a specification for append.
Jim Bowery
OK, slogging through Naish's paper, I encounter:
"The key to defining formal semantics for (predicate) logic programming
languages is to define what atoms are true."
and the from
http://www.clip.dia.fi.upm.es/phd/slides/96_3_prolog_language/node2.html
"In Prolog, the term ``atom'' is applied to the constants in the program"
Something isn't working here.
Carl Alphonce
In article <jaboweryE...@netcom.com>,
I encountered the same difficulty recently when reading different
texts. Naish is referring to a semantic notion of atomicy, as
is usual in logic: atoms are atomic formulas, like pred(X,Y,Z),
whose truth value is non-decomposable. It is common in a logic
programming context to make use of a syntactic notion of atomicity.
An atomic formula like pred(X,Y,Z) is decomposable into the name
of the relation, "pred" and the variables "X", "Y" and "Z" and
punctuation symbols.
You will notice also that in a term as used in logic programming
is also defined syntactically, while in logic a distinction is
made between terms (which refer to individuals in your domain
of discourse) and formulae (which have truth values).
While in logic terms and formulae are distinguished syntactically
(the sets of function and predicate symbols are disjoint),
they are distinguished by context in, say, Prolog. Thus, it
is possible to write
f(f(a)).
without ambiguity. The outer f is a predicate symbol, while the
inner f is a function symbol.
Has there been any attempt to standardize terminology?
Carl Alphonce
---
Carl Alphonce / email: alph...@cs.ubc.ca
Department of Computer Science / phone: (604) 822-8572
University of British Columbia / FAX: (604) 822-5485
Vancouver, BC, CANADA, V6T 1Z4 / http://www.cs.ubc.ca/spider/alphonce/home
--
Carl Alphonce
Jim Bowery
Carl Alphonce (alph...@cs.ubc.ca) wrote:
: I encountered the same difficulty recently when reading different
: texts. Naish is referring to a semantic notion of atomicy, as
: is usual in logic: atoms are atomic formulas, like pred(X,Y,Z),
: whose truth value is non-decomposable.
Well, it looks like _someone_ has to be a militant ignoramous around
here and, as usual, I get the short lot. ;-)
KMorris692
In article <60abuo$7...@mulga.cs.mu.OZ.AU>, f...@mundook.cs.mu.OZ.AU (Fergus
Henderson) writes:
>Clearer than the formal specification?
>
>I don't know about you, but I certainly find English a lot easier to
>read than predicate calculus. I'm pretty sure I'm not alone in this.
>
>Formal specifications are _precise_, but not necessarily easy to understand.
However, my experience is that humans tend to be poor at expressing
themselves rigorously in prose. Heck, I've met college English instructors
who cannot spell reliably. It gets even worse than this: Jon Bentley opined
in a 1980's ACM or IEEE journal column (Programming Pearls), and I saw
first-hand, that given the ability to program directly in logic we'd see
that programmers are not logical.
One can create a formal language that uses an English-based vocabulary and
syntax, but I wouldn't count that as prose.
I agree that prose companions to formal specifications can be quite
helpful, but if I can have only one, I'd pick specifications in an
appropriate formal language over specifications in prose.
Fergus Henderson
kmorr...@aol.com (KMorris692) writes:
>f...@mundook.cs.mu.OZ.AU (Fergus Henderson) writes:
>
>>Clearer than the formal specification?
>>
>>I don't know about you, but I certainly find English a lot easier to
>>read than predicate calculus. I'm pretty sure I'm not alone in this.
>>
>>Formal specifications are _precise_, but not necessarily easy to understand.
>
>However, my experience is that humans tend to be poor at expressing
>themselves rigorously in prose.
Oh, for sure. I'm not suggesting that formal specifications are a bad idea.
I was just pointing out that the fact that a specification is formal
does not necessarily make it clear; to make our formal specifications
as clear as possible, we need to choose appropriate formal languages.
Expressing *everything* directly in predicate calculus does not necessarily
give the clearest specification. It can be appropriate to use a slightly
different language to express the types than the language we use to express
other parts of the specification.
--
Norbert E. Fuchs
In article <19970924211...@ladder01.news.aol.com>,
kmorr...@aol.com (KMorris692) wrote:
>In article <60abuo$7...@mulga.cs.mu.OZ.AU>, f...@mundook.cs.mu.OZ.AU (Fergus
>Henderson) writes:
>
>>Clearer than the formal specification?
>>
>>I don't know about you, but I certainly find English a lot easier to
>>read than predicate calculus. I'm pretty sure I'm not alone in this.
>>
>>Formal specifications are _precise_, but not necessarily easy to understand.
>
>However, my experience is that humans tend to be poor at expressing
>themselves rigorously in prose. Heck, I've met college English instructors
>who cannot spell reliably. It gets even worse than this: Jon Bentley opined
>in a 1980's ACM or IEEE journal column (Programming Pearls), and I saw
>first-hand, that given the ability to program directly in logic we'd see
>that programmers are not logical.
>
>One can create a formal language that uses an English-based vocabulary and
>syntax, but I wouldn't count that as prose.
>
>I agree that prose companions to formal specifications can be quite
>helpful, but if I can have only one, I'd pick specifications in an
>appropriate formal language over specifications in prose.
>----
> "Communication is possible only between equals." -- Hagbard Celine
Would this count as prose for you?
...
If a book is checked out to a borrower and a staff user returns it then
the book is available.
If a staff user adds a book to the library then the book is available
and the staff user creates a catalog entry that contains the author of
the book and the title of the book and the subject of the book and the
id of the book.
If a book is available and a staff user removes the book from the library
then the staff user deletes the catalog entry of the book and the book is
not available.
...
In case you are wondering - this is an excerpt of Kemmerer's library data
base specification problem expressed in Attempto Controlled English. It is
completely - and automatically - translatable into predicate logic.
--
Norbert E. Fuchs
Department of Computer Science
University of Zurich
CH-8057 Zurich
Switzerland
Telephone +41-1-635 43 13
Fax +41-1-635 68 09
mail fu...@ifi.unizh.ch
WWW http://www.ifi.unizh.ch/staff/fuchs.html
Jim Bowery
Any rational specification system would work interactively, going
automatically back and forth between controlled natural language (CNL) and
formal logic, so that the end result is a clear and intended natural
language specification that translates directly to formal logic.
Isn't it interesting that this is exactly what the inventors of
formal logic said they set out to do originally -- and that no one
has actually DONE IT yet?
KMorris692
In article <60cmtb$r...@mulga.cs.mu.OZ.AU>, f...@mundook.cs.mu.OZ.AU (Fergus
Henderson) writes:
>Oh, for sure. I'm not suggesting that formal specifications are a bad idea.
>I was just pointing out that the fact that a specification is formal
>does not necessarily make it clear; to make our formal specifications
>as clear as possible, we need to choose appropriate formal languages.
>Expressing *everything* directly in predicate calculus does not necessarily
>give the clearest specification. It can be appropriate to use a slightly
>different language to express the types than the language we use to express
>other parts of the specification.
Thanks for clarifying your position. I think we mostly agree; I certainly
agree with you that it is wise to consider using more than one language
when it would aid clarity (or even brevity). I was merely railing about the
almost certain loss of completeness and correctness when using ordinary
prose instead of more formal languages.
----
"Communication is possible only between equals." -- Hagbard Celine
Karen A. Morrissey
KMorr...@aol.com
303-753-2968
KMorris692
In article <fuchs-25099...@rzuppppri1-13.unizh.ch>,
fu...@ifi.unizh.ch (Norbert E. Fuchs) writes:
>Would this count as prose for you?
>[...]
>If a book is checked out to a borrower and a staff user returns it then
>the book is available.
>
>If a staff user adds a book to the library then the book is available
>and the staff user creates a catalog entry that contains the author of
>the book and the title of the book and the subject of the book and the
>id of the book.
>
>If a book is available and a staff user removes the book from the library
>then the staff user deletes the catalog entry of the book and the book is
>not available.
> [...]
>In case you are wondering - this is an excerpt of Kemmerer's library data
>base specification problem expressed in Attempto Controlled English. It is
>completely - and automatically - translatable into predicate logic.
If the vocabulary, syntax, and semantics are formally defined, then I
would consider this a prose-like formal language. I once read that the
prose specifications for Algol were quite rigorous because the principal
author's native language was not English (the language of the spec). The
author chose to be exceptionally consistent in his choices of words and
phrases because he realized that if he wasn't consistent then native
English readers might infer unintended, subtle, incorrect, additional
meaning to the specification.
I think that formalized natural language is quite reasonable, so long as
the formal meanings of sentences are (almost) always reasonable meanings of
the same sentences taken as ordinary prose.
Jim Bowery
In business processes, or other privileged rule systems, one has
authority to alter rules to be in accordance with rationality as
discovered during the interactive specification process I described
earlier. As I pointed out, this isn't automated to the degree that it
could be and really should be. Some people have bitten off a much more
difficult problem, and found it too difficult to chew, let alone swallow
-- but their efforts and failures might be instructive in the context of
"intended meaning" in logic programming -- especially as they make direct
reference to logic programming as their formalism:
http://cleo.murdoch.edu.au/asu/edtech/cleo_web/mdomo/elaw-j.arcs/greinke.txt
Jim Bowery
In Naish's paper, it is said of the program:
append([],A,A) :- list(A).
append(A.B,C,A.D) :- append(B,C,D).
"The cost of the extra test whenever append are called is highly
undesirable. In most calls to append all arguments must be lists and in
other cases the programmer can add an extra call to list."
For those of us who believe a compiler can infer, from "list(A)", that
the arguments to append must be lists, the first sentence is not to the
point. Indeed, if one replaces the syntactic sugar of the period
operator with "head" and "tail" predicates, it becomes apparent that
"list" is an abstraction, related to the predicates "head" and
"tail" rather than anything peculiar to primitive types. Therefore, the
second sentence seems confused to those of us with this particular
immunity to Naish's mental virus.
How might one modify these two sentences to render the NIV (Naish
Intellectual Virus) more virulent?
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>In Naish's paper, it is said of the program:
>
>append([],A,A) :- list(A).
>append(A.B,C,A.D) :- append(B,C,D).
>
>"The cost of the extra test whenever append are called is highly
>undesirable. In most calls to append all arguments must be lists and in
>other cases the programmer can add an extra call to list."
>
>For those of us who believe a compiler can infer, from "list(A)", that
>the arguments to append must be lists, the first sentence is not to the
>point.
In Naish's type system, that inference would not be valid.
For example, the following program is type-correct according
to Naish's type system:
null(0).
null([]).
p :- null(X), append(Xs, Ys, Zs).
This program calls `append' with an argument that might or might not
be a list.
Jim Bowery
Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
: For example, the following program is type-correct according
: to Naish's type system:
: null(0).
: null([]).
: p :- null(X), append(Xs, Ys, Zs).
: This program calls `append' with an argument that might or might not
: be a list.
Are you sure you entered this example correctly?
Jim Bowery
I'm going to assume that "Xs" should have been "X" in the example:
Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
: For example, the following program is type-correct according
: to Naish's type system:
: null(0).
: null([]).
: p :- null(X), append(X, Ys, Zs).
: This program calls `append' with an argument that might or might not
: be a list.
Let's dispense with the notion of "list(X)" as a concrete type and
talk about it as an abstract type.
Why isn't it true that:
list(X) :- null(X).
?
If it _is_ true, then the compile time inference allows that polymorphism
in the abstraction.
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>I'm going to assume that "Xs" should have been "X" in the example:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>: For example, the following program is type-correct according
>: to Naish's type system:
>
>: null(0).
>: null([]).
>
>: p :- null(X), append(X, Ys, Zs).
>
>: This program calls `append' with an argument that might or might not
>: be a list.
>
>Let's dispense with the notion of "list(X)" as a concrete type and
>talk about it as an abstract type.
>
>Why isn't it true that:
>
>list(X) :- null(X).
>
>?
Because null(0) is true but list(0) is not.
I constructed null/1 specifically so that list(X) <= null(X)
would not be true. It was just an example of the consequences
of the way Naish's system allows arbitrary supertypes and subtypes.
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>: For example, the following program is type-correct according
>: to Naish's type system:
>
>: null(0).
>: null([]).
>
>: p :- null(X), append(Xs, Ys, Zs).
>
>: This program calls `append' with an argument that might or might not
>: be a list.
>
>Are you sure you entered this example correctly?
Sorry, the `X' should be `Xs'.
p :- null(Xs), append(Xs, _Ys, _Zs).
Jim Bowery
: >
: >Why isn't it true that:
: >
: >list(X) :- null(X).
: >
: >?
: Because null(0) is true but list(0) is not.
: I constructed null/1 specifically so that list(X) <= null(X)
: would not be true.
Yes I see that. I'm asking "why" at a deeper level -- at the
level of the intended meaning of "list(0)".
: It was just an example of the consequences
: of the way Naish's system allows arbitrary supertypes and subtypes.
In the context of "intended meaning" arbitrary flexibility is not to
the point.
Here is something that _is_ to the point, so you understand what I'm
trying to discuss:
i = [1,1,1,1,1,1,1,1]
j = [1,1,1,1,1,1,1,1]
i as a list is obviously equal to j as a list.
However, i as a one's compliment integer (0) is not equal to j as a two's
compliment integer (-1). Obviously i and j are not even equal to
themselves if viewed under these two systems of representation.
If the raw predicate calculus is enhanced with nothing more than a 3
place equality axiom, such as, "X equals Y as Z" we can construct all
of finite mathematics (credit to T. Etter in forthcoming paper).
I suggest that with something like this simple form of equality theory, we
can construct not only all of finite mathematics, but a type system that
handles polymorphism quite naturally. Where Naish's type system fits into
this scheme, I'm not yet sure, but I don't see where his type syntax is
presented with the sugars that convert it, along with the program, into
the raw predicate calculus. If the absence of such sugars is what you
meant by "two languages" I have to disagree that it is an appropriate way
to approach the problem of semantics and the intended meaning of
specifications.
So, getting back to your example of:
null(0).
null([]).
We could define a separate predicate:
equalAsList(X,Y) :- null(X),null(Y).
equalAsList... etc.
and then say:
append([],A,A) :- equalAsList(A,A).
or, alternatively, we could simply claim that we _should_ define
list(X) :- null(X)
list... etc.
At this stage, I'd be hapy to see either of these examples debunked by
something other than a definitional or tautological argument --
specifically by rewording the sentence in Naish's paper that makes
reference to the execution time overhead of such checks so that those of
us who would like to see such checks optimized out at compile time anyway
aren't left wondering why the inefficiency of such type checks is used by
Naish as a motive for the rest of his work.
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>: jabo...@netcom.com (Jim Bowery) writes:
>: >Let's dispense with the notion of "list(X)" as a concrete type and
>: >talk about it as an abstract type.
>: >
>: >Why isn't it true that:
>: >
>: >list(X) :- null(X).
>: >
>: >?
>
>: Because null(0) is true but list(0) is not.
>
>: I constructed null/1 specifically so that list(X) <= null(X)
>: would not be true.
>
>Yes I see that. I'm asking "why" at a deeper level -- at the
>level of the intended meaning of "list(0)".
Well, the intended meaning of list(X) is that X is a list, and 0 is
not a list; the intended meaning of `null(Y)' is that Y is a value
that can be considered to be a "null" value, i.e. 0 or [].
>If the raw predicate calculus is enhanced with nothing more than a 3
>place equality axiom, such as, "X equals Y as Z" we can construct all
>of finite mathematics (credit to T. Etter in forthcoming paper).
>
>I suggest that with something like this simple form of equality theory, we
>can construct not only all of finite mathematics, but a type system that
>handles polymorphism quite naturally.
Well, it is possible, but I'd really have to see the details to be
convinced.
>Where Naish's type system fits into
>this scheme, I'm not yet sure, but I don't see where his type syntax is
>presented with the sugars that convert it, along with the program, into
>the raw predicate calculus.
The sugar used in Naish's type system is very simple.
Basically you just conjoin the type constraints with the
clauses to get the predicate calculus meaning.
A declaration such as
:- type t ---> a ; b ; c where (Y : goal(Y)).
is sugar for
has_type(X, t) :- (X = a ; X = b ; X = c), (X = Y, goal(Y)).
A declaration such as
:- pred p(t1, t2) where (p(A, B) : goal(A, B)).
p(X, Y) :- goal2(X, Y).
is sugar for
p(X, Y) <=
has_type(X, t1), has_type(Y, t2),
(p(X, Y) = p(A, B), goal(A, B)),
goal2(X, Y).
If you are dealing with negation, then you might also want to take the
completion; in that case it would be
(has_type(X, t1), has_type(Y, t2), (p(X, Y) = p(A, B), goal(A, B))
=> (p(X, Y) <=> goal2(X, Y)).
>So, getting back to your example of:
>
>null(0).
>null([]).
>
>We could define a separate predicate:
>
>equalAsList(X,Y) :- null(X),null(Y).
>equalAsList... etc.
>
>and then say:
>
>append([],A,A) :- equalAsList(A,A).
>
>or, alternatively, we could simply claim that we _should_ define
>
>list(X) :- null(X)
>list... etc.
Neither of those definitions would match my intended semantics for
append/3 and list/1.
According to my intended semantics, append/3 and list/1 only succeed
for lists, so `null(X), append(X, _, _)' and `null(X), append(_, X, _)'
should succeed only for X = [], not for X = 0.
Because the type system allows subtypes, it is necessary to perform
run-time type checks when converting from a supertype to a subtype.
Any system that allows arbitrary types (i.e. one in which type are arbitary
sets), rather than just regular types, will allow subtypes. So any system
that allows arbitrary types will have the same problem.
For another example, if I have a predicate `merge' which expects its
arguments to be sorted, then if you want to stick with just predicate
calculus, the intended semantics must be that it fails if the arguments
are not sorted. And that means that either the predicate or its caller
must ensure that the arguments are indeed sorted. In general, a compiler
won't be able to infer that, so if it is to be checked, the check must
be at runtime.
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>
>>Jim Bowery wrote:
>>>In Naish's paper, it is said of the program:
>>>
>>>append([],A,A) :- list(A).
>>>append(A.B,C,A.D) :- append(B,C,D).
>>>
>>>For those of us who believe a compiler can infer, from "list(A)", that
>>>the arguments to append must be lists, the first sentence is not to the
>>>point.
>>
>>In Naish's type system, that inference would not be valid.
>
>Now I understand what you meant when you said this... You meant
>that it might not be possible to do the compile-time type check.
>Yes. Absolutely. And that's why you would go ahead and NOT optimize
>out the call to list(X) for those callers who supplied arguments whose
>types could not be guaranteed as lists.
Well, now this optimization is getting a bit trickier...
but probably still quite doable, I guess.
The cases where it is not doable are for non-regular types.
Naish's argument about efficiency does hold in that case.
>>For example, the following program is type-correct according
>>to Naish's type system:
>>
>> null(0).
>> null([]).
>>
>> p :- null(X), append(X, Ys, Zs).
>>
>>This program calls `append' with an argument that might or might not
>>be a list.
>
>Calling this "type correct" seems an unusual usage of "type" since
>X is really a typeless argument (intersection rather than super or sub).
Yes, Naish's usage of "type" and "type correct" are definitely
a rather non-standard usage!
>: For another example, if I have a predicate `merge' which expects its
>: arguments to be sorted, then if you want to stick with just predicate
>: calculus, the intended semantics must be that it fails if the arguments
>: are not sorted. And that means that either the predicate or its caller
>: must ensure that the arguments are indeed sorted. In general, a compiler
>: won't be able to infer that, so if it is to be checked, the check must
>: be at runtime.
>
>Absolutely. No argument here.
But having the check at runtime is in many cases prohibitively expensive.
(e.g. in the case of merge, doing the check at runtime would double the
number of comparisons required... and there are many examples which are
a lot worse.)
So the moral is that you should not stick with just predicate calculus;
instead you should separate out the types from the other parts of the code.
That allows you to be more efficient, since you only have to be sound
for type-correct programs, rather for all programs, and you can leave
it up to the programmer to prove type-correctness in the difficult
(non-regular type) cases.
Jim Bowery
: >out the call to list(X) for those callers who supplied arguments whose
: >types could not be guaranteed as lists.
: Well, now this optimization is getting a bit trickier...
: but probably still quite doable, I guess.
: The cases where it is not doable are for non-regular types.
: Naish's argument about efficiency does hold in that case.
And by "non-regular" I take it you mean types where the behavior is quite
convoluted in terms, not of the set of operations that can be applied so
much as the structure of those operations as determined by the structure
of the data, say for example directed graphs and acyclic trees. Various
kinds of arbitrary constraints that you may want to impose on these very
general types -- constraints that may be rather difficult to express in
conventional "type" terms, but types which could be constructed as a type
check expression in the predicate calculus quite readily -- its just that
you don't want to actually have to execute the check expression at run
time, and it would do no good at compile time because of the difficulties
in theorem derivation which humans are better at than the compiler
algorithms.
OK, so now the question is, what to do in the "type language" to deal
with this pragmatic issue. The difference as I see it between Naish
and myself is that I believe one should program the type checks in
as though they were going to be executed all the time at run-time --
and that when one departs from the predicate calculus (or its bastardized
version ala prolog) one does so in order to provide the compiler
with the information it needs to optimize the run-time type checks
out of existence. But this doesn't mean one should preempt the compiler's
optimizer and remove them yourself by extracting the type checks into
a separate language.
Basically, something like a compiler directive which can be inserted in
the body of a predicate stating something like "assume(sorted(X))" would
suffice for the irregular types -- "haveFaithThat(sorted(X))" if you want
to assert your human superiority at theorem derivation.
Jim Bowery
Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
: Well, the intended meaning of list(X) is that X is a list, and 0 is
: not a list; the intended meaning of `null(Y)' is that Y is a value
: that can be considered to be a "null" value, i.e. 0 or [].
Ah. It sounded like you had wanted the call to append with 0
to succeed, so I was trying to make sense on that basis.
Earlier you said:
>Jim Bowery wrote:
>>In Naish's paper, it is said of the program:
>>
>>append([],A,A) :- list(A).
>>append(A.B,C,A.D) :- append(B,C,D).
>>
>>For those of us who believe a compiler can infer, from "list(A)", that
>>the arguments to append must be lists, the first sentence is not to the
>>point.
>
>In Naish's type system, that inference would not be valid.
Now I understand what you meant when you said this... You meant
that it might not be possible to do the compile-time type check.
Yes. Absolutely. And that's why you would go ahead and NOT optimize
out the call to list(X) for those callers who supplied arguments whose
types could not be guaranteed as lists.
>For example, the following program is type-correct according
>to Naish's type system:
>
> null(0).
> null([]).
>
> p :- null(X), append(X, Ys, Zs).
>
>This program calls `append' with an argument that might or might not
>be a list.
Calling this "type correct" seems an unusual usage of "type" since
X is really a typeless argument (intersection rather than super or sub).
Yes, of course the program calls append with an argument that might or
might not be a list -- but neither would any compiler be able to infer
list(X) from null(X), so the example I gave would NOT optimize out the
call to list(X) at compile time, and it would be "well typed" in the same
sense that you describe: it would have to do the run-time call to list(X)
as part of append([],A,A):-list(A). Now what was that Naish said about
the run-time overhead of calling list(A) being highly undesirable?
: run-time type checks when converting from a supertype to a subtype.
So what the compiler generates is two versions of append([],A,A): 1) that
called by bindings where A is inferred at compile time to be a list, 2)
that called by bindings where A is inferred at compile time to possibly be
a list. This is similar to what any compiler will do that supports
generic procedure calls.
: Any system that allows arbitrary types (i.e. one in which type are arbitary
: sets), rather than just regular types, will allow subtypes. So any system
: that allows arbitrary types will have the same problem.
Yes, this is not a complaint against Naish's system... it is a necessary
consequence of his attempt to do the right thing. He should be careful in
his criticisms of run-time overhead of type checks, which I don't believe
he was when he worded the sentence I've been obsessing about and which you
made reference to when you first introduced Naish's work in this forum.
Glass houses and all that...
: For another example, if I have a predicate `merge' which expects its
: arguments to be sorted, then if you want to stick with just predicate
: calculus, the intended semantics must be that it fails if the arguments
: are not sorted. And that means that either the predicate or its caller
: must ensure that the arguments are indeed sorted. In general, a compiler
: won't be able to infer that, so if it is to be checked, the check must
: be at runtime.
Absolutely. No argument here. By the way, you might want to look into
the category theoretic definition of a sorted list. A lot of people are
really hot on category theory as the basis for some of this stuff. I
tend to agree, but I'd like to see how far simple enhancements to the
predicate calculus get us first, mainly because of the nice mapping onto
natural languages and relational databases -- stuff that is in widespread
industrial use now.
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>OK, so now the question is, what to do in the "type language" to deal
>with this pragmatic issue. The difference as I see it between Naish
>and myself is that I believe one should program the type checks in
>as though they were going to be executed all the time at run-time --
>and that when one departs from the predicate calculus (or its bastardized
> version ala prolog) one does so in order to provide the compiler
>with the information it needs to optimize the run-time type checks
>out of existence. But this doesn't mean one should preempt the compiler's
>optimizer and remove them yourself by extracting the type checks into
>a separate language.
True, that is not the only possible solution. But it seems like a fairly
pragmatic one to me.
>Basically, something like a compiler directive which can be inserted in
>the body of a predicate stating something like "assume(sorted(X))" would
>suffice for the irregular types -- "haveFaithThat(sorted(X))" if you want
>to assert your human superiority at theorem derivation.
That would be possible, but I suspect that it might lead to less readable
programs that Naish's approach.
Note that since there is a simple translation from program+types to
predicate calculus, there is no loss of generality with Naish's approach.
One issue to consider is that because some assumptions will not be
checked in the body of a procedure, it becomes the responsibility of
the caller of that procedure to ensure that those assumptions are
satisfied. In other words, those assumptions are part of the
interface of the procedure, not just its implementation.
Thus it may be better to write them somewhere else than in the body
of the procedure.
Jim Bowery
: >the body of a predicate stating something like "assume(sorted(X))" would
: >suffice for the irregular types -- "haveFaithThat(sorted(X))" if you want
: >to assert your human superiority at theorem derivation.
: That would be possible, but I suspect that it might lead to less readable
: programs that Naish's approach.
: Note that since there is a simple translation from program+types to
: predicate calculus, there is no loss of generality with Naish's approach.
First of all, I disagree that there is no loss of generality. You lose
Prolog's inherent polymorphism which derives from its search algorithm.
Secondly, choosing the appropriate sugars is important in any case and it
should be obvious I'm not real hot on any particular sugar here, but on an
underlying point:
Programmers should include all the logic in their programs to ensure
logical correctness. Yes, that means compilers should optimize, and yes
compilers can't do an adequate job without human insight and guidance.
Picking the right sugars for this is important, but you had best
not lose sight of the more fundamental problems which are logical
completeness and optimization via theorem derivation/inference.
: One issue to consider is that because some assumptions will not be
: checked in the body of a procedure,
No anguage feature will make up for a programmer that
doesn't complete the logic of his program.
: it becomes the responsibility of
: the caller of that procedure to ensure that those assumptions are
: satisfied.
No, it becomes the responsiblity of the programmer to to his job and
it is the responsibility of the language designer to help him in
that task.
It is less difficult to write:
append([],A,A):-list(A).
than it is to write:
append(A,B,C) type list(A), list(B), list(C).
append([],A,A).
The former is more general because it doesn't get in the way of
alternative implementations of append that require different types for its
arguments. This sort of alternative searching is an inherent strength of
Prolog which generates polymorphism. I see Naish's system as working at
cross purposes with that inherent polymorphic strength -- not with it, his
discussion of polymorphism in his paper notwithstanding.
: In other words, those assumptions are part of the
: interface of the procedure, not just its implementation.
: Thus it may be better to write them somewhere else than in the body
: of the procedure.
These assumptions should be specified differently for each different
implementation of the abstraction so that polymorphism isn't compromised
and so that the logic of the program is complete. The proper place for
this is in the implementation itself rather than some global interface
specification that stomps on polymorphism.
Naish says of type inference in 6.8.1:
"The schemes based purely on type inference cannot be easily compared with
our scheme... Our view is that the program does not fully specify the
intended semantics, and that types supplied by the programmer are needed
for this."
As far as I can see, this all goes back to 2 issues, both of which
I have addressed repeatedly and at length:
1) Naish's statement "The cost of the extra test whenever append (is) called
is highly undesirable." is simply not to the point since the compiler
should optimize such tests out of existence -- so the only reason
"that the program does not fully specify the intended semantics"
is because the programmer is gun-shy of inadequate compiler design.
2) In order to optimize such tests out of existence the compiler needs
help from the human doing inferences -- but this is a problem that
goes beyond "types" as Naish has conceived them and extends to the
general domain of programming and compiler optimization. So dealing
with "types" is a partial and inadequate solution to this problem
while providing a way for the human to provide inferential assertions
is complete and adequate given the fact that the program is fearlessly
complete in its logic.
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>: jabo...@netcom.com (Jim Bowery) writes:
>: >Basically, something like a compiler directive which can be inserted in
>: >the body of a predicate stating something like "assume(sorted(X))" would
>: >suffice for the irregular types -- "haveFaithThat(sorted(X))" if you want
>: >to assert your human superiority at theorem derivation.
>
>: That would be possible, but I suspect that it might lead to less readable
>: programs that Naish's approach.
>
>: Note that since there is a simple translation from program+types to
>: predicate calculus, there is no loss of generality with Naish's approach.
>
>First of all, I disagree that there is no loss of generality. You lose
>Prolog's inherent polymorphism which derives from its search algorithm.
You lost me there. What do you mean by "Prolog's inherent polymorphism"?
>Programmers should include all the logic in their programs to ensure
>logical correctness.
Agreed. But they must also include all the necessary code in their programs
to ensure that the operational behaviour is sound with respect to their
intended declarative semantics. It is not enough for the program to be
logically correct if the implementation is unsound. And your suggestion
of putting hints such as `assumed(some_goal)' in the body of a procedure
means that the implementation will not be sound unless some_goal is true.
>: One issue to consider is that because some assumptions will not be
>: checked in the body of a procedure, it becomes the responsibility of
>: the caller of that procedure to ensure that those assumptions are
>: satisfied.
>
>No, it becomes the responsiblity of the programmer to to his job and
>it is the responsibility of the language designer to help him in
>that task.
I think you missed my point here.
What the language designer needs to do to satisfy the responsibility
of helping the programmer do his job is to make sure that any
assumptions (such as `assumed(some_goal)') are part of the procedure
interface, rather than just hidden in the procedure implementation.
Otherwise, the programmer won't be able to reuse code easily;
the programmer would need to understand the implementation of every
procedure they want to reuse, rather than being able to just look at
the interface.
>It is less difficult to write:
>
>append([],A,A):-list(A).
>
>than it is to write:
>
>append(A,B,C) type list(A), list(B), list(C).
>append([],A,A).
The former may be shorter in this case, but I suspect it is likely to
be more error-prone. With the former syntax, it is probably easy to
forget some type constraints.
(Incidentally the NU-Prolog type checker, which was Naish's implementation
of his system, used the syntax `:- pred append(list, list, list)',
which is slightly less verbose than
`append(A,B,C) type list(A), list(B), list(C)'.)
>The former is more general because it doesn't get in the way of
>alternative implementations of append that require different types for its
>arguments.
I don't see the difference. Why is `list(A)' less general if it is in
the type declaration rather than in the procedure body?
Naish's type system allows types to be specified by arbitrary predicates.
>: In other words, those assumptions are part of the
>: interface of the procedure, not just its implementation.
>: Thus it may be better to write them somewhere else than in the body
>: of the procedure.
>
>These assumptions should be specified differently for each different
>implementation of the abstraction
If that were the case, then in general you wouldn't be able to substitute one
implementation for another, because that might lead to unsoundness
(as described above).
This seems to me to be a bad property. You ought to be able to substitute
different implementations of an abstraction. If you can't do that, then
this suggests to me that perhaps there is something wrong with your notion
of abstraction.
Lee Naish
In article <jaboweryE...@netcom.com>, jabo...@netcom.com (Jim Bowery) writes:
> Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
> : Note that since there is a simple translation from program+types to
> : predicate calculus, there is no loss of generality with Naish's approach.
>
> First of all, I disagree that there is no loss of generality.
There is no loss of generality. Anything you can do with the "rely on a fancy
compiler" option you can do with the declaration option.
> You lose
> Prolog's inherent polymorphism which derives from its search algorithm.
I, like Fergus, don't follow this.
> Programmers should include all the logic in their programs to ensure
> logical correctness.
Thats what the theoreticians have always said. They even said people did it.
The main point of my paper was that people don't do it (often for efficiency
reasons) and by using my scheme we can have the semantics specified, correctness
criteria clear and no runtine overhead is necessary.
> It is less difficult to write:
>
> append([],A,A):-list(A).
>
> than it is to write:
>
> append(A,B,C) type list(A), list(B), list(C).
> append([],A,A).
If all predicates had a single clause containing only a single variable like
this case then I agree: that particular declaration syntax is a big loser. If
you look at the declarations supported in the NU-Prolog Debugging Environment
(which are designed for a practical system, not a paper which concentrates on
semantics) there is less difference. If you look at procedures with more
clauses and more variables in their heads you will see that declarations are a
big winner. They also make maintaining the code much easier, are a useful source
of documentation, allow better syntactic sugar, etc etc.
> As far as I can see, this all goes back to 2 issues, both of which
> I have addressed repeatedly and at length:
>
> 1) Naish's statement "The cost of the extra test whenever append (is) called
> is highly undesirable." is simply not to the point since the compiler
> should optimize such tests out of existence -- so the only reason
> "that the program does not fully specify the intended semantics"
> is because the programmer is gun-shy of inadequate compiler design.
The paper was originally written over ten years ago. At that time types in
any shape or form were not well accepted in the LP community. There are still
no compilers which optimize such tests out of existence, as far as I know,
though I beleive my paper referred to work by Dart and Zobel which did
precisely this in many cases. Its difficult enough to convince people to
include type information in their programs even if you give them the incentive
of debugging tools. Perhaps making their programs compile and run slower will
convince them (bloated software *is* popular), but I doubt it.
> 2) In order to optimize such tests out of existence the compiler needs
> help from the human doing inferences -- but this is a problem that
> goes beyond "types" as Naish has conceived them and extends to the
> general domain of programming and compiler optimization. So dealing
> with "types" is a partial and inadequate solution to this problem
> while providing a way for the human to provide inferential assertions
> is complete and adequate given the fact that the program is fearlessly
> complete in its logic.
By far the most common criticism of my paper has been that "types" as I
conceived them extend to the general domain of programming and hence they
are too general. Its hard to please everybody! My "type" definition language
is Turing complete and its possible to adopt a programming style where
virtually all of the reasoning about program correctness is embodied in the
proof of type correctness (which in general is undecidable). See
@incollection{naish:verif:90,
author = {Naish, Lee},
title = {Verification of logic programs and imperative programs}
,
booktitle = {Constructing logic programs},
editor = {Jean-Marie Jacquet},
publisher = {Wiley},
address = {Chichester, England},
year = {1993},
pages = {143-164},
documentURL = "http://www.cs.mu.oz.au/~lee/papers/verify/tr.ps.gz",
comment = {Technical Report 90/6, Department of Computer
Science, University of Melbourne}
}
lee
Jim Bowery
: >Prolog's inherent polymorphism which derives from its search algorithm.
: You lost me there. What do you mean by "Prolog's inherent polymorphism"?
When Prolog searches for a series of alternative unifications with the
same functor, it is actually looking for different implementations, each
with a potentially different domain (and/or different range) and/or a
different set of internally-used operations.
Types are generally discussed in terms of either a set of values, or of a
set of operations. When you declare a type, you are usually putting
together a set expression of some kind. In most languages, prior to
polymorphism's ascendancy, you put together a set of values. In more
recent languages, such as Objective C and Java, you have these things
called "protocols" which are really a set of operations. I like protocols
better than types because I like polymorphism, but I'm suspicious of both
of these approaches -- especially when Prolog offers an alternative
via the OR part of the and/or logic which is more general as long as
you implement it in a way that is actually useful to good designers
and good programmers (the AND part of the and/or logic doing intersection
rather than union operations for your polymorphic "type" construction).
Something that glares at us in all the prior discussions is the fact that
the two versions of append are actually insisting on two different
"types" of input arguments for different domains of "append"'s space.
There are all kinds of ways one can conceive of constructing different
implementations of the same mapping using different internal operations,
since this is really the entire basis of algebra -- and that invalidates
the use of protocols for such polymorphisms.
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>: jabo...@netcom.com (Jim Bowery) writes:
>: >First of all, I disagree that there is no loss of generality. You lose
>: >Prolog's inherent polymorphism which derives from its search algorithm.
>
>: You lost me there. What do you mean by "Prolog's inherent polymorphism"?
>
>When Prolog searches for a series of alternative unifications with the
>same functor, it is actually looking for different implementations, each
>with a potentially different domain (and/or different range) and/or a
>different set of internally-used operations.
>
>Types are generally discussed in terms of either a set of values, or of a
>set of operations. When you declare a type, you are usually putting
>together a set expression of some kind.
OK. But the polymorphism can be in the types, just as easily as it
can be in the clauses. So there is no loss of generality in Naish's
approach.
>I like protocols
>better than types because I like polymorphism, but I'm suspicious of both
>of these approaches -- especially when Prolog offers an alternative
>via the OR part of the and/or logic which is more general
Ah. Now this is heading the discussion in an entirely different
direction. Originally, the stated premise of the discussion was that
types were arbitrary sets. Now you are criticising other approaches.
This widens the scope of the discussion.
Certainly Naish's approach is more general than other approaches.
That's exactly its problem! It is _too_ general.
With Naish's approach, type-correctness becomes undecidable.
And the results I've observed in practice are that type errors slip
past the type checker.
Protocols (or equivalently Java interfaces, or Haskell type classes,
or sometime in the not-too-distant future Mercury type classes ;-)
seem to me to be a better approach. They allow polymorphism
but still give you a decidable type system.
>There are all kinds of ways one can conceive of constructing different
>implementations of the same mapping using different internal operations,
>since this is really the entire basis of algebra -- and that invalidates
>the use of protocols for such polymorphisms.
I must say that you lost me here again.
I don't see why you couldn't use protocols for that kind of polymorphism.
In fact it seems to me that protocols are designed for exactly that
kind of situation.
Regarding the claimed loss of generality with protocols, well,
I'd be more inclinded to believe it if there were practical examples.
Jim Bowery
: >set of operations. When you declare a type, you are usually putting
: >together a set expression of some kind.
: OK. But the polymorphism can be in the types, just as easily as it
: can be in the clauses. So there is no loss of generality in Naish's
: approach.
Here is where Naish and I disagree on pragmatics. "can be" doesn't mean
"will be in practice". Naish thinks real programmers given a smart
compiler won't include all the logic in the clauses. I think real
programmers, given any kind of compiler, won't include all the types that
are actually used by their programs. If you get into real world problems
with lots of disorganized data, Prolog shines precisely because it can,
with sufficiently rich logic, sort through the gunk and extract useful
abstractions - after a bunch of failed unifications.
: >I like protocols
: >better than types because I like polymorphism, but I'm suspicious of both
: >of these approaches -- especially when Prolog offers an alternative
: >via the OR part of the and/or logic which is more general
: Ah. Now this is heading the discussion in an entirely different
: direction. Originally, the stated premise of the discussion was that
: types were arbitrary sets. Now you are criticising other approaches.
: This widens the scope of the discussion.
Well, I did mention protocols and my desire to focus more on defining
types in terms of operations than in terms of sets, but Naish's approach
is just fine in either regard -- its a good type system -- I just don't
like type systems per se.
: Certainly Naish's approach is more general than other approaches.
: That's exactly its problem! It is _too_ general.
: With Naish's approach, type-correctness becomes undecidable.
: And the results I've observed in practice are that type errors slip
: past the type checker.
OK, now we may be discovering a more important underlying disagreement.
I don't think Naish's system is general enough because I think
real world problems are uncooperative when it comes to fitting our type
semantics (normal database schemas). This "car" has a doggie in the
window whose head bobs up and down when it goes over bumps, and those
cars don't. Yes, you can set up a "type" that includes the
"bobbingHeadAnimalInWindow" attribute/operation, but it is kind of silly to
do so. As I said before, SunSoft's "Self" programming language is
instructive in this regard.
: Protocols (or equivalently Java interfaces, or Haskell type classes,
: or sometime in the not-too-distant future Mercury type classes ;-)
: seem to me to be a better approach. They allow polymorphism
: but still give you a decidable type system.
I don't care about decidability per se --I just want the compiler to give
me as much information as it can within the allotted time -- specifically
on logic inconsistencies, within the program and between the program and
my assertions about the program. Sugar to taste but don't forget what
you are doing is the equivalent of what Cyc does when it pops out with
semantic inconsistencies every morning for the linguistics programmers
when they come in to do the day's work. (I'm ignoring optimization here
to focus on the more essential point that people worry about in type
systems.)
: >There are all kinds of ways one can conceive of constructing different
: >implementations of the same mapping using different internal operations,
: >since this is really the entire basis of algebra -- and that invalidates
: >the use of protocols for such polymorphisms.
: I must say that you lost me here again.
: I don't see why you couldn't use protocols for that kind of polymorphism.
: In fact it seems to me that protocols are designed for exactly that
: kind of situation.
: Regarding the claimed loss of generality with protocols, well,
: I'd be more inclinded to believe it if there were practical examples.
A simple example would be the expressions:
(sqrt(3-x)*2)**2
vs
(3-x)*4
Algebraically equivalent except the first one fails for values of x<3 and
it uses sqrt and **. If you don't have sqrt and ** defined for some
representation of number you are using, or x<3, the first
"implementation" fails. But its simply incorrect to claim that sqrt and
** must be part of the "protocol" in the abstract -- because you have an
alternative implementation that works for implementations without sqrt
and **, and for subdomains <3.
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>: I must say that you lost me here again.
>: I don't see why you couldn't use protocols for that kind of polymorphism.
>: In fact it seems to me that protocols are designed for exactly that
>: kind of situation.
>
>: Regarding the claimed loss of generality with protocols, well,
>: I'd be more inclinded to believe it if there were practical examples.
>
>A simple example would be the expressions:
>
>(sqrt(3-x)*2)**2
>
>vs
>
>(3-x)*4
>
>Algebraically equivalent except the first one fails for values of x<3 and
>it uses sqrt and **. If you don't have sqrt and ** defined for some
>representation of number you are using, or x<3, the first
>"implementation" fails. But its simply incorrect to claim that sqrt and
>** must be part of the "protocol" in the abstract -- because you have an
>alternative implementation that works for implementations without sqrt
>and **, and for subdomains <3.
Ah. That's a kind of silly example, because there's not much reason
to use the more complicated expression. But I know some similar examples
that are realistic; for example containers implemented as hash tables,
if a hashing operation is available, or as trees, if a comparison operation
is available, or as lists otherwise.
Protocols work fine for this sort of thing, so long as you have
a way of checking whether a type supports a particular protocol
(or, in other terminology, conforms to a particular interface,
or is a member of a particular type class).
The interface specifies the minimal protocol necessary to implement
the operation. The implementation can then check whether more
sophisticated protocols are available, and if so, it can use them;
if not, it can fall back to the implementation using the minimal protocol.
Jim Bowery
Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
: The interface specifies the minimal protocol necessary to implement
: the operation. The implementation can then check whether more
: sophisticated protocols are available, and if so, it can use them;
: if not, it can fall back to the implementation using the minimal protocol.
OK, so I chose a "silly" example that you found a way around. How about
intersection sets of operations, as opposed to subsets?
Lee Naish
In article <61g7nh$2...@mulga.cs.mu.OZ.AU>, f...@mundook.cs.mu.OZ.AU (Fergus Henderson) writes:
> Certainly Naish's approach is more general than other approaches.
> That's exactly its problem! It is _too_ general.
> With Naish's approach, type-correctness becomes undecidable.
> And the results I've observed in practice are that type errors slip
> past the type checker.
Thats because the particular *implementation* is very simple - a few hours
work. There is no reason why it could not be extended so that it analysed
regular types in a "complete" way (as well as doing other incomplete analysis).
You would then catch *all* the errors that would be caught using a more restricted
framework for types *plus more*. Type errors can also slip past the Mercury type
checker - its just that the Mercury people refuse to call these errors type
errors. Using a flexible type definition language (as I proposed) gives the
potential of detecting more errors. By restricting the type definition language
you reduce the potential set of errors which can be detected, and even if you
fully achieve this potential, you are still not detecting all possible errors.
Fergus has also made the mistake of linking the type checker in NUDE/ntc with
type correctness. That type checker has nothing to do with checking type
correctness. Type correctness (as defined in my paper) is undecidable even if
the type definition language is extremely weak (eg no recursion allowed, so all
types must be finite). All type checking algorithms either reject programs which
work or accept programs which don't work (due to type errors). Strong type
checking systems (eg, Mercury) do both - some programs are considered ill-typed
even though they would work under Prolog and other programs with type errors
are considered well-typed because the type system cannot express all the type
information (eg, integer sub-ranges).
I'm not saying that Mercury is a bad. Its is a good compromise amongst many
options. However, when talking about "type errors" I think a lot of people
concentrate on their own favourite type scheme and miss the bigger picture.
lee
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>: The interface specifies the minimal protocol necessary to implement
>: the operation. The implementation can then check whether more
>: sophisticated protocols are available, and if so, it can use them;
>: if not, it can fall back to the implementation using the minimal protocol.
>
>OK, so I chose a "silly" example that you found a way around. How about
>intersection sets of operations, as opposed to subsets?
I don't know exactly what you mean here.
It would help if you give an example.
Fergus Henderson
l...@cs.mu.OZ.AU (Lee Naish) writes:
>f...@mundook.cs.mu.OZ.AU (Fergus Henderson) writes:
>> Certainly Naish's approach is more general than other approaches.
>> That's exactly its problem! It is _too_ general.
>> With Naish's approach, type-correctness becomes undecidable.
>> And the results I've observed in practice are that type errors slip
>> past the type checker.
>
>Thats because the particular *implementation* is very simple - a few hours
>work. There is no reason why it could not be extended so that it analysed
>regular types in a "complete" way (as well as doing other incomplete analysis).
Normally when you talk of "extending" a language, or a type system,
you mean increasing the set of programs that it accepts. But an
"extension" of the sort you suggest above would reduce the set of
programs that it accepts. So I'd call that a restriction, not
an extension.
Yes, if you restricted your system in this manner, then it would
no longer be too general.
>Using a flexible type definition language (as I proposed) gives the
>potential of detecting more errors.
Yes, and I agree it is a good idea. It's even on my list of things to do...
But for a practical system, it is better to start with a system that
can be extended to the ideal point rather than starting with a system
that is too general and later restricting it. The latter approach has
some rather unfortunate backwards compatibility problems ;-)
>Fergus has also made the mistake of linking the type checker in NUDE/ntc with
>type correctness. That type checker has nothing to do with checking type
>correctness.
My complaint was that the NUDE/ntc type checker didn't report errors
for some programs that were not type-correct. I suppose I should
have been complaining that the NUDE/ntc type checker didn't report errors
for some programs that were not _regular-type-correct_. Here by
"regular-type-correctness" I mean type correctness as defined by some
strong regular type system, e.g. the Mercury type system.
Apologies if that wasn't clear.
Jim Bowery
: I don't know exactly what you mean here.
: It would help if you give an example.
OK, another silly example:
x*x+1
x**2+1
What is the "minimal protocol"?
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>: jabo...@netcom.com (Jim Bowery) writes:
>: >How about intersection sets of operations, as opposed to subsets?
>
>: I don't know exactly what you mean here.
>: It would help if you give an example.
>
>OK, another silly example:
>
>x*x+1
>
>x**2+1
>
>What is the "minimal protocol"?
If you do want compile-time type safety, then you can make the
operations you need into a new protocol. You could write this example
as `sqr(x) + 1', where `sqr' is a method from a new type-class (protocol)
called say `squarable'.
The disadvantage of this approach is that unless the system supports
overlapping instance declarations (which most don't -- there are good
reasons not to), you may need a lot of different instance declarations
to say which types are instances of the type-class `squarable'.
If you don't need compile-time type safety, you can use an empty
protocal, check for support of the `*' and `**' protocols,
and if the type supports neither, report an error.
-- pseudocode
foo x =
if has_op '*' x then
x*x+1
else if has_op '**' x then
x**2 + 1
else
error
Actually it would be quite possible to use this approach and still
get compile-time checking, if the compiler did a little bit of
partial evaluation.
Jim Bowery
Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
: If you don't need compile-time type safety, you can use an empty
: protocal, check for support of the `*' and `**' protocols,
: and if the type supports neither, report an error.
: -- pseudocode
: foo x =
: if has_op '*' x then
: x*x+1
: else if has_op '**' x then
: x**2 + 1
: else
: error
: Actually it would be quite possible to use this approach and still
: get compile-time checking, if the compiler did a little bit of
: partial evaluation.
I prefer:
sqrinc(X,Y) :- sqr(X,X2),inc(X2,Y).
sqrinc(X,Y) :- mul(X,X,X2),inc(X2,Y).
Let success/failure sort it out.
Fergus Henderson
jabo...@netcom.com (Jim Bowery) writes:
>Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
>: If you don't need compile-time type safety, you can use an empty
>: protocal, check for support of the `*' and `**' protocols,
>: and if the type supports neither, report an error.
>
>: -- pseudocode
>: foo x =
>: if has_op '*' x then
>: x*x+1
>: else if has_op '**' x then
>: x**2 + 1
>: else
>: error
>
>: Actually it would be quite possible to use this approach and still
>: get compile-time checking, if the compiler did a little bit of
>: partial evaluation.
>
>I prefer:
>
>sqrinc(X,Y) :- sqr(X,X2),inc(X2,Y).
>sqrinc(X,Y) :- mul(X,X,X2),inc(X2,Y).
>
>Let success/failure sort it out.
In other words, not only do you not want compile time error checking,
you don't even want run time error checking?
Well, good luck. And good luck to whoever has to maintain your programs
when you are gone ;-)
Jim Bowery
Fergus Henderson (f...@mundook.cs.mu.OZ.AU) wrote:
: In other words, not only do you not want compile time error checking,
: you don't even want run time error checking?
Your comment is consistent with your perception that we've changed the
subject and it is why I consider this discussion of protocols part of the
prior discussion on compile time inference vs type declaration.