Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!ames!uhccux!munnari.oz.au!cs.mu.oz.au!ok
From: ok@cs.mu.oz.au (Richard O'Keefe)
Newsgroups: comp.lang.prolog
Subject: Re: Semantics of type checking (was "extralogical")
Keywords: usage
Message-ID: <2483@munnari.oz.au>
Date: 21 Oct 89 05:03:38 GMT
References: <2204@munnari.oz.au> <786@ecrcvax.UUCP> <2390@munnari.oz.au> <1213@kuling.UUCP>
Sender: news@cs.mu.oz.au
Lines: 54

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.