This document gives a short introduction to the system T Y P I C A L for Annotated Prolog The aim of Typical is to do static type checking on logic programs. The software will check Prolog programs that are extended with type declarations. The type system includes subtyping and parametric polymorphism. A description of the general idea and of the techniques for type checking and type inferencing can be found in two technical reports ([1],[2], see below). Installation and license notes and examples can be found in the files INSTALL and LICENSE. See also the file LIMITATIONS for some technical limitations of the current version of the software. This file belongs to version 0.4 ========================================================================= An annotated Prolog program consists of *) type definitions, and *) predicate type declarations, and *) Prolog clauses as usual, and an *) optional module structure 0) Operator syntax ------------------ The type syntax uses several operators, which are defined in the file 'typeops'. In order to ensure that these operators are defined, when a program is fed into a conventional Prolog system, a program file should start with :- ensure_loaded(typeops). 1) Type definitions ------------------- All types and the corresponding function symbols must be defined. The basic form of a type definition is an enumeration of the symbols type color --> red; green; blue. which defines a type 'color' with three symbols 'red', 'green', and 'blue' of type 'color'. If a function symbol has arguments, then the corresponding types must be given in the definition. type machine --> fastm(int,string); slowm(int,string). Subtype relationships between types are defined by 'subtype' phrases. In order to define the type 'negint' as subtype of 'int', one can write subtype negint < int. or (equivalent) type negint < int. All terms having the type 'negint' will be of type 'int' implicitly. If a type is completely defined by its subtype, i.e., there are no functions symbols assigned directly to that type, then type int. suffices to define the type name. For convenience, subtyping can also be written as `supertyping' suptype int > nat. or type int > nat. Parametric types can be defined by using type variables in the definitions, e.g. type bintree(T) --> leaf(T); bnode(T, bintree(T), bintree(T)) . defining a tree of elements having some type 'T'. The ubiquitous list is defined by type list(T) --> [] ; [ T | list(T) ]. Note that infix notation for operators and types mix well. Parametric types can be ordered in the same way as other types. However, the parameters of parametric types that have a subtype relation must be the same. E.g., if binary trees are modelled as a subtype of trees in general, this can be expressed as subtype bintree(T) < tree(T). A complete type definition for trees and binary trees could look like type bintree(T) --> leaf(T) ; bnode(T,bintree(T),bintree(T)). type tree(T) --> node(T,list(tree(T))). suptype tree(T) > bintree(T). While types are usually defined by enumerating the function symbols belonging to that type, it is also possible to specify the terms by a goal expression, e.g. type posint --> {X|(integer(X),X>0)}. A term 'X' has type 'posint' if the goal expression '(integer(X),X>0)' is true. I.e., 'posint' contains the set of all 'X' such that ... Types can have aliases defined by type alias = original. type alias == original. Any occurrence of the type name 'alias' will be replaced by 'original' internally. A type alias should not be part of a subtype relationship or defined through -->. The type definitions above are essentially written as Prolog predicates. Appropriate operator definitions in the file 'typeops' allow for some syntactical sugar. All type definitions can also be written as Prolog directives, i.e. starting with ':-'. The type checker will handle both syntactical styles with no difference. E.g., the directives :- type color --> red; green; blue. :- type colour == color. :- subtype thing < color. are as good as type color --> red; green; blue. type colour == color. subtype thing < color. Both styles can be mixed. Directives for defining types emphasize the fact that types definitions do not affect the semantics of some Prolog program as given by a set of clauses. Written in the syntax without a leading ':-' type definitions look like type definitions in other languages. The choice is left to the personal taste of the programmer. Directives tend to be more compatible with various Prolog systems. E.g., Quintus Prolog wants ':- multifile' directives for 'type', 'subtype' etc. in _all_ files where these operators are used without a leading ':-'. 2) Predicate declarations ------------------------- Predicate declarations specify the types which are expected for the actual arguments when a predicated is called. E.g., if the first argument of a predicate 'sumlist' must be a list of integers and the second argument must be an integer, the declaration is pred sumlist( list(int), int ). Declarations may contain type parameters, written as conventional Prolog variables, e.g., for 'app' pred app( list(T), list(T), list(T)). A subgoal 'app(L1,L2,L3)' is type consistent if there is a (ground) instance 'list(atype)' for 'list(T)' such that 'L1' and 'L2' and 'L3' have the type 'list(atype)'. More specific type declarations are possible by using so-called anchored type parameters, marked by '@', and type constraints as in pred append(list(@T1),list(@T2),list(@T)) -> T1 =< T, T2 =< T. or pred append(list(@T1),list(@T2),list(@T)) with T1 =< T, T2 =< T. The operators '->' and 'with' can be used interchangeably. In order to check if a subgoal 'append(L1,L2,L3)' is type consistent, the type inference determines the least types of all arguments. These least types are matched with the corresponding type terms in the declaration. If the type constraints are satisfiable in the type order, then the subgoal is type consitent. There is a simple syntactic abbreviation for anchored parameters: Every non-anchored parameter T in the predicate part is implicitly replaced by a new anchored parameter @Tnew and a constraint Tnew =< T is added to the constraint part. Hence the previous declaration for append is equivalent to pred append(list(T),list(T),list(@T)) . Each predicate should have a type declaration. The definitional genericity condition (see ref. [2]) is applied to all clauses by default. This condition can be relaxed for specific clauses by using an appropriate pragma, see below. If the predicate of the head atom in a clause has a declaration starting with the keyword (i.e., operator) 'predl' instead of 'pred', the genericity condition is not applied to the clause as well. 3) Prolog clauses ----------------- The type system does not impose any restrictions on the Prolog clauses. If a predicate declaration constains type parameters, the type checker assumes that all defining clauses for that predicate are generic, i.e., they are type consistent for every instance of the type parameter. If a clause is not intended to be generic, then a subgoal type_pragma(non_generic) should be added to the clause in the program. Then the type checker will check if there is any instance for the parameters in the predicate declaration such that the clause is type consistent. Furthermore, if the type checker shall ignore a clause for some reason, then a subgoal type_pragma(nocheck) can be added to the clause. Clauses containing this subgoal will always be considered as type consistent. When the Prolog program is executed any subgoal of the kind 'type_pragma(Anykey)' will always succeed. It is implemented as a fact 'type_pragma(_).' in the file 'typeops'. 4) Options ---------------------- The type checker 'tap' can be called with several options [no options given] tap checks input file and writes error messages if type-inconsistencies or other problems are found -v print clauses while they are checked and also print variable typings for each clause -dummy-pdecl don't complain abount missing predicate declarations default declarations, with all arguments having type 'top', are used. -dummy-fdecl don't complain about undeclared function symbols default declarations, with all arguments having type 'top' and result type 'top', are used. 5) Module structure ------------------- The module structure in the current version of Typical is rather tentative. Because modules are not standardized for Prolog and commonly used statements, such as module/1 in SICStus and Quintus Prolog, do not fit well for our purpose, Typical uses an own syntax. The declarations contained in any file can be imported with the statements :- type_import(a_file_name). or :- type_impex(a_file_name). The default file extensions, such as ',pl', are tried, hence 'type_import(myfile)' will read 'myfile.pl'. Multiple default directories containing imported files can be defined, hence libraries do not have to exist in the working directory (see installation hints). More than one file can be imported by using an appropriate import statement for each file. If an imported file contains further import statements, then these imports are handled recursively. The type checker tries to read each file at most once, even if it occurs in more than one import statement. A file may contain type declarations abstract type aname --> Constructors. which will be handled as abstract type definitions where this declaration is imported. I.e., the name of the type is known but not the Constructors The same applies to type renamings abstract type aname == anything. Type definitions and predicate declarations which are preceded by the operator 'local', such as local type my --> mycons. local pred p(int). are not exported. ======================================================================= Built-in types -------------- type goal --> "any Prolog goal". type top --> "any Prolog term". Not built-in yet ---------------- type void == goal. % O'Keefe compatible type any == top. ======================================================================= References: [1] Meyer, Gregor; On the use of types in logic programming Technical report 199, Fernuniversit"at Hagen, June 1996 [2] Meyer, Gregor; Type checking and type inferencing for logic programs with subtypes and parametric polymorphism. Technical report 200, Fernuniversit"at Hagen, June 1996 The current version of Typical and TeX-dvi and PostScript copies of ref. [1] and [2] are available at the URL http://www.fernuni-hagen.de/pi8/typical/