Types for Prolog

There's been quite a discussion on types over at comp.lang.Prolog. In my opinion types are essential for programming in the large. The lack of types is one of the reasons for making Prolog a small language.

So Prolog should have types that are statically enforced. What types? I'd rather not invent an awkwardly ad-hoc type system that fits existing code patterns. In order to make types work a lot for you, you must work a little too. What I mean is that certain programming style must be adopted that is not necessarily the anything-you-write-is-fine style of an untyped language. So why invent a new type system if we can reuse a tried-and-true one: the Hindley-Milner type system. It's been around for about 30 years, and applied with success in several languages. In particular, it's being used in Mercury, and it works!

Of course, we don't want to switch from Prolog to Mercury overnight. There's all the legacy code we don't have the time and money to port. Moreover, Mercury's demand for declarations is pretty heavy weight: not only types are demanded, but also modes and determinism.

That's why I started a type checker library in (SWI-)Prolog: type_check.pl. Include this library in your code, and you can use Mercury-style type declarations and predicate signatures.

Basic use the library

In order to use the type checker, you must include the library in your module:

:- use_module(type_check).

This way the type checker will be run whenever you load your library. Any type errors it finds, will be reported during the loading process.

Now, before you can use any types, you must defined them. This is done using Mercury-style type definitions. There are two forms. The first form is for defining a new algebraic data type. E.g.

:- type list(T) ---> [] ; [T|list(T)].

defines a polymorphic type of lists. Note that this particular type is already predefined by the type_check library, as well as a few others (integer/0, boolean/0 and pair/2, for now).

The second form is for defining an alias (type alias) of another type. E.g.

:- type intlist == list(integer).

defines a shorter name intlist for the type list(integer). For the type checker these two are equal.

Once you have defined the types you need, you can use them to write signatures for your predicates. E.g.

:- pred mem(E,list(E)).

states that mem/2's first argument is of any one type E and mem/2's argument is of type list(E). With the signature in place, you can happily write the predicate definition:

mem(X,[X|_]).
mem(X,[_|T]) :- mem(X,T).

Now load your module, and the type checker verifies wether the predicate definition conforms to the predicate signature. If it doesn't, it complains with an error message. There is no further runtime overhead (like runtime assertions): well-typed code can't go wrong.

Assume that I wrote the first clause as (the arguments switched):

mem([X|_],X).

When I load the file, I get the error message:

TYPE ERROR: expected type `list(list(_G759))' for term `_G730'
           inferred type `_G759'
       in head `mem([_G730|_G733], _G730)' of clause:
mem([A|_], A).

Admittedly, the error messages are currently far from the most informative, but this project has just begun. Your suggestions for improvement and patches are much appreciated.

Untyped legacy code

Of course, we still have that untyped legacy code. We don't want to type all that code, let alone rewrite it to make it typable. That's why I added the ability to have typed and untyped code interact in a safe manner:

• When untyped code calls the typed code, a runtime test is performed right before the call to check whether the call is well-typed. This also holds for calls from the Prolog toplevel!
  
• When typed code calls untyped code, you must annotate the call with a singature. A runtime check will then verify whether the call behaves according to its signature.
  

This was inspired by Phil Waddler's recent paper, which establishes that well-typed code is not to blame. Any type errors will be caught at the interface between the untyped and the typed code, and the untyped code is to blame.

You can find a fully annotated library module for binomial heaps here. It's a port from Haskell code.