🚀 go-pugleaf

In article <1213@kuling.UUCP>, mattias@emil.CSD.UU.Se (Mattias Waldau) writes:

> What is the semantics of type checking?

There are two basic observations.
(a) Some built-in predicates may report an error if called with
    inappropriate arguments.  For example, arithmetic comparisons
    in DEC-10 Prolog print an error message if any variable in
    them is bound to something other than a number.  Precisely
    which predicates report errors and which fail quietly is, alas,
    implementation dependent.  But at the very least "well-typed
    programs do not go wrong" means that calls to built in predicates
    in well-typed programs never report type errors.

(b) Some predicate definitions are really not intended as what they
    appear to be.  The standard example of this is append/3, which
    is not intended to be used on anything other than lists.  Every
    non-trivial program I have checked is riddled with predicates
    whose definitions are only correct under certain implicit
    assumptions (this argument is non-zero, that argument occurs in
    this other, and so on).

My interest in type checking was that Leon Sterling had written a small
Boyer-Moore-style theorem prover for Horn Clause programs, and most of
the theorems I wanted it to prove turned out to be non-theorems because
of (b).

> Should a ill-typed program fail or is it an error?

Why should I define it?  The only behaviour of an ill-typed query is
"rejected as ill-typed"; what _would_ happen if it was allowed to run
is unobservable.  In a *well*-typed program, neither type failure nor
type error can occur.

> If the HCMT program corresponds to (2) type checking is used to assure
> that all calls of q during the execution are defined.

That is one purpose for using a type checker.

> If the HCMT
> program corresponds to (3) type checking is just partial evalutation,
> we are moving execution to compile-time.

As I was interested in "supplementing" the bare rules with further
constraints which ensured that the theorems I wanted to be true were
in fact true, that is the view I took.

It's worth noting that the Mycroft/O'Keefe paper only considers Horn
Clauses and SLD; it does _not_ consider negation nor yet SLDNF.  I
imagine that the choice between (2) and (3) does matter if you are
handling negation.  Lee Naish has found that some problems in that
case; adding type declarations to a Horn Clause program causes at
most a monotonic decrease in the model, but this is not so for programs
with negation.  I have no idea (yet) what to do about that.