Prolog Type Checker

Appeared in Volume 10/2, May 1997

Keywords: typing.

rwab1@cl.cam.ac.uk
Ralph Becket
30th November 1996

I've written a typechecker to aid in debugging Prolog programs. Type systems help make programs more readable and can be used to spot a large class of coding errors. For more information and a pointer to the source code, please take a look at:
http://www.cl.cam.ac.uk/users/rwab1/prolog/typechecker.html

I strongly encourage people to try it out - I've found it an invaluable development and debugging aid.

fjh@mundook.cs.mu.oz.au
Fergus Henderson
30th November 1996

People who are interested in this tool may also be interested in using the '--typecheck-only' option of the Mercury compiler to typecheck their Prolog programs.

Ralph Becket's typechecker uses almost exactly the same syntax as the Mercury typechecker. There are a number of differences, however; perhaps the most important one is that the Mercury typechecker does static ("compile-time") type checking or type inference, whereas Becket's tool does dynamic checking at runtime.

See http://www.cs.mu.oz.au/mercury for details on how to obtain the Mercury compiler.

rwab1@cl.cam.ac.uk
Ralph Becket
2nd December 1996

Agreed - my system only performs dynamic typechecking. As such it is intended as a debugging tool for use with existing bodies of code where adding full type information to a largish set of programs is either too expensive or even impossible. Having said that, there is no reason why it should not also come in handy for smaller programs.

From what I've seen of Mercury , I would definitely recommend anyone starting a new project to use it instead of Prolog. Mercury is the Right Way to Go! But if you're stuck with Prolog, some protection (such as typechecker) is better than none at all.

Gregor.Meyer@FernUni-Hagen.de
Gregor Meyer
3rd December 1996

I did some experiments with the typechecker using the following example:

:- pred imem(integer,list(integer)).
:- pred member(T,list(T)).
p :- imem(not_an_int,[1,2,3]).
q :- member(not_an_int,[1,2,3]).

When p is executed the debugging tool will find a type error. That's fine. However, when q is executed, no error is detected and q simply fails. Most people will find that the clause for q is ill-typed for obvious reasons. With a flat, i.e. many-sorted, type system, there is no instance of the type parameter T such that the atom member(not_an_int,[1,2,3]) is well-typed.

Because Ralph's typechecker also includes a type 'any', it essentially uses an ordered type-hierarchy and the implementation will find (automatically) that the atom member(not_an_int,[1,2,3]) is well-typed with respect to member(any,list(any)).

I think that the typechecker should never instantiate type parameters to 'any'.

Fergus Henderson wrote:
Becket's tool does dynamic checking at runtime.

I have implemented a tool for static type analysis of Prolog, which allows ordered types and refined predicate declarations. More information can be found at: http://www.fernuni-hagen.de/pi8/typical/

rwab1@cl.cam.ac.uk
Ralph Becket
3rd December 1996

Gregor Meyer writes:
the typechecker should never instantiate type parameters to 'any'.

I'm afraid that the inclusion of 'any' was driven by pragmatic reasons rather than aesthetic ones. Part of my work is with a 500K+ line Prolog system and there is no way I, or anyone else, is going to annotate that lot! The reasons my typechecker contains the type 'any' and performs dynamic rather than static typechecking are two-fold:

It is intended for use after-the-fact to aid in debugging new code written by a number of people for an existing system.
It is often the case that when checking user input, or automatically manipulating Prolog programs, you want to know if someone has broken the rules. This is hard to check statically.

Gregor has also told me that he believes that static and dynamic typecheckers work well in a complementary fashion.

No Next