🚀 go-pugleaf

In article <6333@goanna.cs.rmit.oz.au> ok@goanna.cs.rmit.oz.au (Richard A. O'Keefe) writes:
>In article <9106111357.AA29175@ucbvax.Berkeley.EDU>, POPX@vax.oxford.ac.uk (Jocelyn Paine) writes:
>> Is there a generally accepted notation for specifying types in Prolog?
>
>No.
>
>> Are any of these programs in wide
>> enough use to merit adopting their notation for types as a de facto
>> standard?
>
>No.  There isn't even wide agreement on what kind of types we ought to
>have.  For what it's worth, Bristol's new Goedel language uses essentially
>the Hindley/Milner/Mycroft types, modulo minor syntactic details.
>
>> If so, are any of them in the public domain? I have the type-checker
>> from Edinburgh Tools, but it relies on some oddities of DEC-10 Prolog
>> (won't run under Poplog for example), and doesn't handle modules.
>
>I am unaware of any dependencies on DEC-10 Prolog.  It took very little
>effort to make it run under C Prolog, Quintus Prolog, SICStus Prolog,
>NU Prolog.  If there are any problems, please let me know.
>
>Of course it doesn't handle modules.  There is even less agreement about
>modules than about types.  (The latest ISO suggestion I've seen is unacceptably
>complex.  I mean by that that if it becomes standard I will join the
>Pop camp and forget about Prolog; it'll be too hard to use reliably.)
>
>As far as I know, the type checker in the DEC-10 Prolog library (what is
>the relationship between the DEC-10 library and "Edinburgh tools"?) is
>the _only_ Prolog type checker which has ever been broadcast on the net.

These postings  and a subsequent posting talk about types for Prolog. 
As this seems to be a topic of interest, I'd like to RE-POST a message
that I posted back in February (Feb 25, 1991 I think). The main point
is that THERE IS AVAILABLE BY FTP, A TYPE-CHECKING AND TYPE-RECONSTRUCTION
PROCEDURE for Typed Prolog along with examples and a supporting document.

Here are the details again. I'd be delighted to hear your comments and 
respond to any queries regarding the type system.

Thanks,

T.K. Lakshman

PS: A paper on Typed Prolog is to appear in ILPS '91 in San Diego, California.
----------------------------------------------------------------------

	 TYPED PROLOG: TYPE CHECKING AND RECONSTRUCTION 
----------------------------------------------------------------------
This is to (RE)announce the availability of a type checking/reconstruction
procedure for TYPED PROLOG: a prescriptively typed logic programming 
language. Some features of TYPED PROLOG: 

	*.  Explicit type declarations (following the syntax 
	of type declarations in the Mycroft-O'Keefe type checker)

	*. Typed Semantics based on many sorted logic.
 
	*. Support for a large subset of Prolog: including the (in)famous 
	cut, not, assert and retract.

	*. A type CHECKING and RECONSTRUCTION procedure based on Milner's
	type checking algorithm for ML. The procedure performs: 

	a. TYPE CHECKING : when given a Typed Prolog program with type 
	declarations for all function and predicate symbols, the procedure 
	type-checks the program based on the type rules of Typed Prolog.

	b. TYPE RECONSTRUCTION : when given a Typed Prolog program where type
	declarations for predicate symbols are omitted, the procedure 
	reconstructs the omitted types. 

The user can essentially write ordinary Prolog programs in the standard
syntax and use the above-mentioned implementation to type-check the programs 
and reconstruct omitted types for predicates. 

----------------------------------------------------------------------
	       OBTAINING THE CODE and THE RELATED PAPER
----------------------------------------------------------------------

The type-checking/reconstruction code is written in Prolog and has been
tested on Quintus Prolog (v 3.0), C Prolog (v 1.4), SB Prolog (v 2.5) and
SICStus Prolog (v 0.7) This type-checking / reconstruction code is 
available via ANONYMOUS FTP as follows: 

Machine:    a.cs.uiuc.edu. (On the login prompt please say anonymous).
Directory:  pub/reddy/typed-prolog 
File:       Types.tar.Z (please don't forget to set BINARY)

The Types.tar.Z file can be tared/uncompressed as follows: 

(uncompress Types.tar.Z; tar xf Types.tar; echo "y" | \
rm Types.tar >/dev/null) &

This  creates the Typed-Prolog directory. This directory contains 
in addition to the type-checking / reconstruction code and examples, a
README file and a dvi and a postscript copy of a related 
Typed Prolog paper.

----------------------------------------------------------------------



-- 
INTERNET   : lakshman@cs.uiuc.edu
OFFICE    : 217-244-5973        MAIL    : Dept. of C.S., DCL, 
				1304 W Springfield Ave, Urbana, Il 61801.
----------------------------------------------------------------------