Typed LP and call/1

Appeared in Volume 7/3, August 1994

Keywords: typing, call.


eep2pc@ee.surrey.ac.uk
Paul Connolly
11th May 1994

In typed logic programming languages how are uses of the predicate call/1 type-checked (if at all)?

I can see the following alternatives:

1) call/1 is not implemented (the minimalist "solution" :-)

2) call/1 is statically type-checked (the very difficult, perhaps imposible, but ideal solution)

3) call/1 is dynamically type-checked (the slow, "leave a hole in the type system" "solution")

Does anyone know how 2) is or might be implemented given that the call functor might be created from a list using =.. ? The possibility of goals being constructed by the program makes this problem more difficult than the usual parametric polymorphism of functional languages (or at least the one's I know about).


fjh@munta.cs.mu.OZ.AU 
Fergus Henderson
18th May 1994

Paul Connolly writes:

1) call/1 is not implemented

Goedel adopts this approach.

He continues:

2) call/1 is statically type-checked

Several languages adopt this approach.

He continues:

Does anyone know how 2) is or might be implemented given that the call functor might be created from a list using =.. ?

I think the languages that adopt (2) tend to disallow `=..'. In fact `call/1' is much easier to fit into a strong type system than `=..'. It's quite straight-forward to allow call/N, which generally makes up for the loss of `=..', at least in as far as it's use to construct terms to be passed to `call/1' is concerned.


ok@goanna.cs.rmit.oz.au 
Richard A. O'Keefe
20th May 1994

Paul Connolly writes:

In typed logic programming languages how are uses of the predicate call/1 type-checked (if at all)?

For the Mycroft/O'Keefe type system, Alan Mycroft and I did actually explain this in the AI Journal '84 paper. The idea is that if

    :- pred p(t1, ..., tn)

and x1, ..., xn are terms of type t1, ..., tn, then

    p(x1, ..., xn)    : void
    p(x1, ..., xn-1)  : void(tn)
    ...
    p(x1)             : void(t2, ..., tn)
    p                 : void(t1, ..., tn)

and the types for the call/N+1 family are

     :- pred call(void(T1,...,Tn), T1, ..., Tn).

He continues:

Does anyone know how 2) is or might be implemented given that the call functor might be created from a list using =.. ?

=.. creates terms, not functors. I presume you mean that the goal passed to call/1 might be created using univ. The problem is univ, not call. The solution is to introduce the call/N+1 family and not make the xxxxing list or call univ in the first place. call/N+1 also lends itself to efficient implementation.

He continues:

The possibility of goals being constructed by the program makes this problem more difficult than the usual parametric polymorphism of functional languages (or at least the one's I know about).

No harder than constructing any other well-typed term. The big problem is univ (almost always a bad idea anyway), functor/3, and arg/3. These are the operations that have no equivalent in the usual functional languages.


P.Connolly@ee.surrey.ac.uk
28th June 1994

The Mycroft/O'Keefe reference is:

Mycroft & O'Keefe, A Polymorphic Type System for Prolog, Artificial Intelligence, Vol 23, No 3, Aug 1984, pp.295 - 307

Perhaps the univ problem might be solved by partial evaluation of the program under type unification, but at the cost of complicating the type system. Fergus Henderson, in an e-mail discussion, was very persuasive in arguing that I might be over-complicating the type system by aiming for such backward compatibility.

No Prev