Typing constraint logic programs.
We present a prescriptive type system with parametric polymorphism and subtyping for constraint logic programs. The aim of this type system is to detect programming errors statically. It introduces a type discipline for constraint logic programs and modules, while maintaining the capabilities of performing the usual coercions between constraint domains, and of typing meta-programming predicates, thanks to the exibility of subtyping. The property of subject reduction expresses the consistency of a prescriptive type system w.r.t. the execution model: if a program is well-typed, then all derivations starting from a well-typed goal are again well-typed. That property is proved w.r.t. the abstract execution model of constraint programming which proceeds by accumulation of constraints only, and w.r.t. an enriched execution model with type constraints for substitutions. We describe our implementation of the system for type checking and type inference. We report our experimental results on type checking ISO-Prolog, the (constraint) libraries of Sicstus Prolog and other Prolog programs.
Introduction
The class CLP(X ) of Constraint Logic Programming languages was introduced
by Jaar and Lassez (Jaar & Lassez, 1987) as a generalization of the innovative
features introduced by Colmerauer in Prolog II (Colmerauer, 1984; Colmerauer,
namely computing in Prolog with other structures than the Herbrand terms,
with inequality constraints and with co-routining.
Inherited from the Prolog tradition, CLP(X ) programs are untyped. Usually the
structure of interest X is however a quite complex combination of basic structures
that may include integer arithmetic, real arithmetic, booleans, lists, Herbrand
terms, innite terms, etc. with implicit coercions between constraint domains
like in Prolog IV (Colmerauer, 1996). Even the early CLP(R) system of (Jaar &
Lassez, 1987) already combines Herbrand terms with arithmetic expressions in a
non-symmetrical way: any arithmetic expression may appear under a Herbrand
function symbol, e.g. in a list, but not the other way around. The framework of
many sorted logic in (Jaar & Lassez, 1987) is not adequate for representing the
type system underlying such a combination, as it forces Herbrand function symbols
Francois Fages and Emmanuel Coquery
to have a unique type (e.g. over reals or Herbrand terms), whereas Herbrand functions
can be used polymorphically, e.g. in f(1) and f(f(1)), or the list constructor
in a list of list of numbers [[3]].
The type system of Mycroft-O'Keefe (Mycroft & O'Keefe, 1984; Lakshman &
Reddy, 1991; Hill & Topor, 1992) is an adaptation to logic programming of the
rst type system with parametric polymorphism, that was introduced by Damas-
Milner for the functional programming language ML. In this system, types are rst-
order terms, type variables inside types, like  in list(), express type parameters.
Programs dened over a data structure of type list() can be used polymorphically
over any homogeneous list of elements of some type . Such a type system for Prolog
is implemented in the systems Godel (Hill & Lloyd, 1994) and Mercury (Somogyi
et al., 1996) for example. The
exibility of parametric polymorphism is however by
far insu-cient to handle properly coercions between constraint domains, such as
e.g. booleans as natural numbers, or lists as Herbrand terms, and does not support
the meta-programming facilities of logic programming, with meta-predicates such
as functor(X,F,N), call(G) or setof(X,G,L).
Semantically, a ground type represents a set of expressions. Subtyping makes
type systems more expressive and
exible in that it allows to express inclusions
among these sets. In this paper we investigate the use of subtyping for expressing
coercions between constraint domains, and for typing meta-programming predi-
cates. The idea is that by allowing subtype relations like list()  term, an atom
like functor([X jL]; F; N) is well-typed with type declaration functor : term
atom  int ! pred , although its rst argument is a list. Similarly, we can type
pred ! pred , freeze : term pred ! pred , setof :  pred  list() ! pred .
The absence of subtype relation list() 6 pred , has for eect to raise a type error
if the call predicate is applied to a list. On the other hand, the subtype relation
pred  term makes coercions possible from goals to terms.
Most type systems with subtyping for logic programming languages that have
been proposed are descriptive type systems, i.e. their purpose is to describe the
success set of the program, they require that a type for a predicate upper approximates
its denotation. On the other hand, in prescriptive type systems, types are
syntactic objects dened by the user to express the intended use of function and
predicate symbols in programs. Note that the distinction between descriptive and
prescriptive type systems is orthogonal to the distinction between type checking
and type inference which are possible in both approaches.
There are only few works considering prescriptive type systems for logic programs
with subtyping (Beierle, 1995; Dietrich & Hagl, 1988; Hanus, 1992; Hill & Topor,
1992; Yardeni et al., 1992; Smolka, 1988). In these systems however, subtype relations
between parametric type constructors of dierent arities, like list()  term,
are not allowed, thus they cannot be used to type metaprogramming predicates
and have not been designed for that purpose. The system Typical (Meyer, 1996)
possesses an ad hoc mechanism for typing metapredicates which makes it quite
di-cult to use. Our objective is to propose a simple type system that allows for a
uniform treatment of prescriptive typing issues in constraint logic programs.
In a prescriptive type system, the property of subject reduction expresses the
Typing Constraint Logic Programs 3
consistency of the type system w.r.t. the execution model: if a program is \well-
typed", then all derivations starting in a \well-typed" goal are again \well-typed".
This is a well-known result of the polymorphic type system without subtyping
(Mycroft & O'Keefe, 1984; Lakshman & Reddy, 1991; Hill & Topor, 1992) but when
subtypes are added to the picture, the absence of a xed data
ow in logic programs
makes the obtention of a similar result problematical. Beierle (Beierle, 1995) shows
the existence of principal typings with subtype relations between basic types, and
provides type inference algorithms, however Beierle and also Hanus (Hanus, 1992)
do not claim subject reduction for the systems they propose. In general types are
kept at run-time (Hanus, 1992; Yardeni et al., 1992) or modes are introduced to
restrict the data
ow (Dietrich & Hagl, 1988; Smaus et al., 2000; Somogyi et al.,
1996).
In this paper, by abstracting from particular structures as required in the CLP
scheme, we study a prescriptive type system for CLP programs, that is independent
from any specic constraint domain X . Section 2 presents the type system that
includes parametric polymorphism and subtype relations between type constructors
of dierent arities, in a quite general type structure of poset with suprema. We show
two subject reductions results. One is relative to the abstract execution model
of constraint programming, which proceeds only by accumulation of constraints.
The proof of subject reduction holds independently of the computation domain,
under the assumption that the type of predicates satises the denitional genericity
principle (Lakshman & Reddy, 1991). The second subject reduction result is relative
to the more concrete execution model of CLP with substitution steps. We show that
for this second form it is necessary to keep at run-time the typing constraints on
variables inside well-typed programs and queries.
Section 3 describes the type checking algorithm and shows that the system of
subtype inequalities generated by the type checker are left-linear and acyclic. Section
4 presents a linear time algorithm for solving left-linear and acyclic systems
of subtype inequalities, and describes the cubic time algorithm of Pottier (Pottier,
2000a) for solving general systems of inequalities, under the additional assumption
that the types form a lattice. Section 5 presents type inference algorithms for
inferring the types of variables and predicates in program clauses.
Section 6 describes our implementation which is available from (Coquery, 2000).
The solving of subtype inequalities is done by an interface to the Wallace constraint-handling
library (Pottier, 2000b). In section 7 we report our experimental results
on the use of this implementation to type check ISO-Prolog, the libraries of Sicstus
Prolog, including constraint programming libraries, and other Prolog programs.
Typed Constraint Logic Programs
In this section we describe our type system as a logic for deriving type judgments
about CLP programs.
4 Francois Fages and Emmanuel Coquery
2.1 Types
The type system we consider is based on a structure of partially ordered terms,
called poterms, that we use for representing types with both parametric polymorphism
and subtype polymorphism. Poterms generalize rst-order terms by the de-
nition of a subsumption order based on function symbols, that comes in addition to
the instantiation preorder based on variables. Poterms are similar to order-sorted
feature terms or -terms (Ait-Kaci & Nasr, 1986; Smolka, 1988; Ait-Kaci et al.,
1997) but we nd it more convenient here to adopt a term syntax (with matching
by position) instead of a record syntax (with matching by name) for denoting static
types.
The set of types T is the set of terms formed over a denumerable set U of
type variables (also called parameters), denoted by ; ; :::, and a nite set of
constructors K, where with each symbol K 2 K an arity m  0 is associated (by
writing K=m). Basic types are type constructors of arity 0. We assume that K
contains a basic type pred . A
at type is a type of the form K(
and the  i are distinct parameters.
The set of type variables in a type  is denoted by V ( ). The set of ground types
G is the set of types containing no variable. We write  [=] to denote the type
obtained by replacing all the occurrences of  by  in  . We write  [] to denote
that the type  strictly contains the type  as a subexpression. The size of a type
, dened as the number of occurrences of constructors and parameters in  , is
denoted by size( ).
We now qualify what kind of subtyping we allow. Intuitively, when a type  is
a subtype of a type  , this means that each term in  is also a term in  . The
subtyping relation  is designed to have certain nice algebraic properties, stated in
propositions below. We assume an order  on type constructors such that: K=m
for each K 2 K the set fK 0 j K  K 0 g has a maximum.
Moreover, we assume that with each pair K=m  K 0 =m 0 , an injective mapping
is associated such that  K;K
whenever K  K 0  K 00 .
These assumptions mean that as we move up in the hierarchy of type constructors,
their arity decreases, and the hierarchy needs not be a lattice but a poset with
suprema.
The order on type constructors is extended to a covariant subtyping order on
types, denoted also by , dened as the least relation satisfying the following rules:
(Par)     is a parameter
(1)  0
Contravariant type constructors could be dened with a subtyping rule similar
to rule Constr but with the ordering relation reversed for some arguments, like
e.g.  (i)   0
i in the premise of the rule for some argument  0
. Such contravariant
type constructors are not considered in this paper.
Therefore, if int  f loat then we have list(int)  list(f loat), list(f loat) 6
Typing Constraint Logic Programs 5
stream_or_alias atom_or_list
stream atom list(A)
character
clause
byte
int
float t_flag
stream_creation_option
stream_property
t_eof_action_or_type
t_eof_action t_type
pred
Fig. 1. Part of the type structure for ISO-Prolog.
list(int), and also list(f loat) 6 list() as the subtyping order does not include the
instantiation pre-order. Intuitively, a ground type represents a set of expressions,
and the subtyping order between ground types corresponds to set inclusion. Parametric
types do not directly support this interpretation, their parameters denote
unkown types.
The type structure given in gure 2.1 represents a part of the types used for type
checking ISO-Prolog. The omitted types are the subtypes of atom associated to all
types, and other types for special values or options. The type list() is the only
parametric type used for ISO-Prolog. Other parametric types are used for typing
Prolog libraries such as arrays(), assoc(; ), heaps(;
etc.
A type substitution  is an idempotent mapping from parameters to types that
is the identity almost everywhere. Applications of type substitutions are dened in
the obvious way.
Proposition 2.1
If    then    for any type substitution .
Proof
By structural induction on  .
Proposition 2.2
If    then size()  size() .
Proof
6 Francois Fages and Emmanuel Coquery
By structural induction on  .
Our assumption that for each K 2 K, the set fK 0 j K  K 0 g has a maximum,
together with the arity decreasing assumption, entail the existence of a maximum
supertype for any type:
Proposition 2.3
For each type  , the set f j   g has a maximum, which is denoted by Max( ).
Proof
By structural induction on  .
This means that every -connected component of types has a root. For example,
a structure like a  b; c  b; c  d violates the hypothesis if b and d have no
common supertype serving as a root for the connected component. On the other
hand that assumption does not assume, nor it is implied by, the existence of a
least upper bound to types having a upper bound (sup-quasi-lattice hypothesis in
(Smolka, 1989)).
Proposition 2.4
For all types  and , Max(
Proof
By structural induction on  .
Note that the possibility of \forgetting" type parameters in subtype relations, as
in list()  term, may provide solutions to inequalities of the form list()  ,
e.g. However, we have:
Proposition 2.5
An inequality of the form    [] has no solution. An inequality of the form
[]   has no solution if
Proof
For any type , we have size() < size( []), hence by Prop 2.2,  6  [], that is
[] has no solution.
For the second proposition, we prove its contrapositive. Suppose  []   has
a solution, say  [=]  . By denition of a maximum and Prop. 2.3, we have
Hence by Prop. 2.4, By the
rules of subtyping we have  6= Max( ). Therefore  62 V (Max( )), since otherwise
would contain Max() as a strict subexpression
which is impossible.
2.2 Well-typed programs
CLP programs are built over a denumerable set V of variables, a nite set F of
function symbols, given with their arity (constants are functions of arity 0), and
a nite set P of program predicate and constraint predicate symbols given with
their arity, containing the equality constraint =. A query Q is a nite sequence of
Typing Constraint Logic Programs 7
constraints and atoms. A program clause is an expression noted A Q where A
is an atom formed with a program predicate and Q a query.
A type scheme is an expression of the form 8 is the set of
parameters in types  We assume that each function symbol f 2 F , has
a declared type scheme of the form 8 is the arity of f , and
is a
at type. Similarly, we assume that each predicate symbol p 2 P has a declared
type scheme of the form 8 !pred where n is the arity of p. The declared
type of the equality constraint symbol is 8u u; u!pred . For notational convenience,
the quantiers in type schemes and the resulting type pred of predicates will be
omitted in type declarations, the declared type schemes will be indicated by writing
, assuming a fresh renaming of the parameters in
for each occurrence of f or p.
Throughout this paper, we assume that K, F , and P are xed by means of
declarations in a typed program, where the syntactical details are insignicant for
our results.
A variable typing is a mapping from a nite subset of V to T , written as
g. The type system denes well-typed terms, atoms and clauses relatively
to a variable typing U . The typing rules are given in Table 1. The rules
basically consist of the rules of Mycroft and O'Keefe plus the subsumption rule.
Note that for the sake of simplicity constraints are not distinguished from other
atoms in this system.
substitution
)Atom  is a type substitution
(Head)
)Head  is a renaming substitution
(Clause)
Query U'A Head

Table

1. The type system.
An object, say a term t, is well-typed if there exist some variable typing U and
8 Francois Fages and Emmanuel Coquery
some type  such that U ' t :  . Otherwise the term is ill-typed (and likewise for
atoms, etc. A program is well-typed if all its clauses are well-typed.
The distinction between rules Head and Atom expresses the usual denitional
genericity principle (Lakshman & Reddy, 1991) which states that the type of a
dening occurrence of a predicate (i.e. at the left of \ " in a clause) must be
equivalent up-to renaming to the assigned type of the predicate. The rule Head used
for deriving the type of the head of the clause is thus not allowed to use substitutions
other than variable renamings in the declared type of the predicate. For example, the
predicate member can be typed polymorphically, i.e. member :  list()!pred , if
its denition does not contain special facts like member(1; [1]), that would force its
type to be member : int  list(int)!pred , for satisfying the denitional-genericity
condition.
The following proposition shows that if an expression other than a clause or a
head is well-typed in a variable typing U , it remains well-typed in any instance U.
Proposition 2.6
For any variable typing U , any type judgement R other than a Head or a Clause,
and any type subtitution , if U ' R then U ' R.
Proof
By induction on the height of the derivation tree for U ' R.
2.3 Subject reduction w.r.t. CSLD resolution
Subject reduction is the property that evaluation rules transform a well-typed expression
into another well-typed expression. The evaluation rule for constraint logic
programming is CSLD-resolution. To recall this evaluation rule, it is convenient to
distinguish in a query Q, the constraint part c (where the sequence denotes the
conjunction) from the other sequence of atoms A. We use the notation
make this distinction. Given a constraint domain X which xes the interpretation
of constraints, a query c 0 jB is a CSLD-resolvent of a query cjA and a (renamed
apart) program clause
and the constraint c
Theorem 2.1 (Subject Reduction for CSLD resolution)
Let P be a well-typed CLP(X ) program, and Q be a well-typed query, i.e. U '
Q Query for some variable typing U . If Q 0 is a CSLD-resolvent of Q, then there
exists a variable typing U 0 such that U 0 ' Q 0 Query.
Proof
Let us assume without loss of generality that that Q 0 is a
CSLD-resolvent of Q with the program clause p(t) djB.
Thus
As Q is well-typed, we have U ' cjp(s); A Query . And as the program is well
Typing Constraint Logic Programs 9
there exists a variable typing U 00 , renamed apart from U , such that U 00 '
p(t) djB Clause .
!pred be the type declaration of predicate p. Since U ' p(s) Atom, we
have substitution .
Now let U . By proposition 2.6, we have U 00  ' djB; Query , thus
What remains to be shown is U
Hence by proposition 2.6, U 00
. Therefore we have U , from which we conclude
It is worth noting that the previous result would not hold without the denitional
genericity condition (expressed in rule Head). For example with two constants a :  a
!pred dened by the non denitional generic
clause p(a), we have that the query p(b) is well typed, but a is a resolvent that
is ill-typed if  a and  b have no upper bound.
2.4 Subject reduction w.r.t. substitutions
The CSLD reductions, noted !CSLD , are in fact an abstraction of the operational
reductions that may perform also substitution steps, noted !  , instead of keeping
equality constraints. As in the CLP scheme constraints are handled modulo logical
equivalence (Jaar & Lassez, 1987), it is clear that the diagram of both reductions
However the previous subject reduction result expresses the consistency of types
w.r.t. horizontal reduction steps only, that is w.r.t. the abstract execution model
which accumulates constraints, but may not hold for more concrete operations
of constraint solving and substitutions. For example, with the subtype relations
int  term, pred  term, the type declarations =:   !pred , int!pred , and
the program p(X), the query
with true, although the query obtained by substitution, p(true), is ill-typed.
In order to establish subject reduction for substitution steps, and be consistent with
the semantical equivalence of programs, one needs to consider a typed execution
model with type constraints on variables checked at runtime. In the example, the
int with the constraint true is unsatisable, the query
Francois Fages and Emmanuel Coquery
will be thus rejected at compile-time by checking the satisability of its typed
constraints.
Denition 2.1
Given a constraint system over some domain X , a typed constraint system over
[2 X is dened by adding type constraints, i.e. expressions of the form t :  where
t is a term and  a type. Basic types are interpreted by distinguished subsets of X
and type constructors by mappings between subsets of X satisfying the subtyping
relation  and the type declarations for function and predicate symbols. A type
there exists a valuation  of the variables in t and
the free parameters in  such that t 2 . A typed constraint system composed
of type constraints and constraints over X is satisable if there exists a valuation
which satises all constraints of the system.
Lemma 2.1
In a typed constraint system,
Proof
For any valuation , if X 2  and
Denition 2.2
The TCLP clause (resp. query) associated to a well-typed program (resp. query)
in a typed environment U is the clause (resp. query) augmented with the type
constraints in U .
Theorem 2.2 (Subject Reduction for substitutions)
Let P be a TCLP program associated to well-typed CLP(X ) program, and Q be a
TCLP query, we have U ' Q Query for some variable typing U . If Q 0 is a CSLD-
resolvent of Q, then the variable typing U 0 associated to the type constraints in Q 0
Query. Furthermore if Q 0 contains an equality constraint
Query.
Proof
Subject reduction for CSLD resolution follows from theorem 2.1 as TCLP programs
are just a special case of well-typed CLP programs. Furthermore one easily checks
that the type constraints in Q 0 , that come from the type constraints in Q and from
the resolving TCLP clause, give exactly the type environment U 0 constructed in
the proof of the previous theorem, thus U Query.
Now let be a constraint in a resolvent Q 0 . Let
in the constraint part of Q 0 which together with by lemma 2.1.
Therefore it is immediate from the typing rules that by replacing X by t in the
derivation of U 0 ' Q 0 Query, and by completing the derivation with the derivation
of we get a derivation of U Query.
The eect of type constraints in TCLP programs is to prevent the derivation of
ill-typed queries by substitution steps. In addition, queries such as
true; p(X) can be rejected at compile-time because of the unsatisability of their
constraints. Similarly TCLP program clauses having unsatisable typed constraints
can be rejected at compile-time.
Typing Constraint Logic Programs 11
Note that in (Smaus et al., 2000) another result of subject reduction for substitutions
is shown without the addition of type constraints but in a very restricted
context of moded logic programs.
3 Type checking
The system described by the rules of Table 1 is non-deterministic, since the rule
(Sub) can be used anywhere in a typing derivation. One can obtain a deterministic
type checker, directed by the syntax of the typed program, simply by replacing the
rule (Sub) by variants of the rules (Func), (Atom) and (Head) with the subtype
relation in their premises. This leads to the following type system in table 2.
substitution
)Atom  is a type substitution
)Head  is a renaming substitution
(Clause)
Query U'A Head

Table

2. The type system in second form.
Proposition 3.1
A program is well typed in the original system if and only if it is well typed in the
new one.
Proof
Clearly, if a program is typable in the new system, it is typable in the original
one: one has just to replace every occurrence of the (Func') and (Atom') rules
respectively with the following derivations:
Francois Fages and Emmanuel Coquery
(Head)
Conversely, if a program is typable in the original system, it is typable in the
second one, noted here ' 2 . The proof is by induction on the typing derivation in
the original system. The rules (Var), (Query) and (Clause) remain the same. The
rule (Atom) and (Head) are similar to rule (Func). We thus show the property for
any term t : if U in the rst system, then U in the second system
with  0   .
Let us consider the three possible cases, either the proof terminates by the application
of the (Var) rule, by the application of the (Func) rule or by application
of the (Sub) rule.
The rst case is trivial as the rule (Var) is the same in both systems.
In the second case, according to the (Func) rule, U '
Then, by the induction hypothesis, the terms t 1    t n are also type checked to
n by the second system, with  0
applying the (Func') rule with  0
In the third case, according to the (Sub) rule, U allows us to
deduce U . By induction hypothesis, t is type checked to U in the
second system, where    . Since    0 , we have    0 . So t is type checked to
The construction of the substitution  needed in rules (Func'), (Atom') and
(Head') for type checking, can be done by solving the system of subtype inequalities
collected along the derivation of a type judgement. The parameters in the type
environment (i.e. the parameters in the types of variables) are however not under
the scope of these substitutions, as they act only on the parameters of the (renamed
declarations for function and predicate symbols. We are thus looking
for type substitutions with a restricted domain. For the sake of simplicity how-
ever, instead of dealing formally with the domain of type substitutions, we shall
simply assume that the parameters in the type of variables are replaced by new
constants for checking the satisability of subtype inequalities, and avoid unsound
instantiations.
Now let  be the collection of subtype inequalities  imposed on types by rules
(Atom') and (Head') in a derivation. Let us dene the size of a system
of inequalities as the number of symbols. The size of the system  of inequalities
associated to a typed program is O(nvd) where v is the size of the type declarations
Typing Constraint Logic Programs 13
for variables in the program, n is the size of the program, and d is the size of the
type declarations for function and predicate symbols.
As the type system is deterministic we have:
Proposition 3.2
A well-formed program is typable if and only the system of inequalities collected
along its derivation is satisable.
It is worth noting that the system of inequalities  collected in this way for type
checking have in fact a very particular form.
Denition 3.1
A system  of inequalities is left-linear if any type variable has at most one occurrence
at the left of  in the system.  is acyclic if there exists a ranking function
on type variables r : U ! N such that if    2 ,
r() < r().
Proposition 3.3
The system of inequalities generated by the type checking algorithm is acyclic and
left-linear.
Proof
As the type variables in the types of CLP variables have been renamed into con-
stants, the only type variables occurring in  are introduced by rules
(Atom') and (Head'), and come from (renamed apart) type declarations of function
and predicate symbols. We can thus associate to each type variable  a rank h()
dened as the height of its introduction node in the derivation tree (i.e. the maximal
distance from the node to its leaves). Now a rule (Func'), (Atom') or (Head')
at height h posts inequalities of the form    , where the rank of the variables in
is h, and the rank of the variables in  is h 1. The system is thus acyclic.
The type variables at the left of  are those parameters that come from the
result type of a function declaration, e.g.  in nil : list(). As the result type is
a
at type, the variables in a result type are distinct and renamed apart, hence
the variables occurring in a type at the left of  have a unique occurrence in the
system. The system is thus trivially left-linear.
Note that if we allowed contravariant type constructors, the previous proposition
would not hold.
A linear time algorithm for solving acyclic left-linear systems is given in the next
section.
4 Subtype inequalities
The satisability of subtype inequalities (SSI) problem is the problem of determining
whether a system of subtype relations 1
n has a
1 The SSI problem should not be confused with the semi-unication problem which is dened with
the instantiation pre-ordering, intead of the subtype ordering: 9
. The
undecidability of semi-unication is shown in (Kfoury et al., 1989).
14 Francois Fages and Emmanuel Coquery
solution, i.e., whether there exists a substitution  such that  i  0
holds for all
Denition 4.1
A solution to an inequality  0 is a substitution  such that  0 . A maximal
solution is a solution  such that for any solution  0 there exists a substitution
such that 8 2 V  0 .
The SSI problem has been deeply studied in the functional programming com-
munity. Due to the lack of results for the general case, special instances of the SSI
problem have been identied along several axes:
the form of the types: basic types, constructor types, covariant (our case in
this paper) or contravariant;
the structure of the types: (disjoint union of) lattices (Tiuryn, 1992), quasi-
lattices (Smolka, 1989), n-crown (Tiuryn, 1992), posets with suprema (our
case), partial orders (Frey, 1997);
the form of the type constraints.
In this section we show that the type constraints generated by the type checking
algorithms can be solved in linear time in our quite general structure of types, and
that the type constraints generated by the type inference algorithms can be solved
in cubic time, under the additional assumption that the types form a lattice.
4.1 The acyclic left-linear case
We show that the satisability of acyclic left-linear subtype inequalities can be
decided in linear time, and admit maximal solutions in our general type structure
posets with suprema.
In this section, we present an algorithm which proceeds by simplication of the
subtype inequalities and introduces equations between a parameter and a type. We
say that a system  is in solved form if it contains only equations of the form
where the  i 's are all dierent and have no other occurrence in . The substitution
associated to a system in solved form  is trivially a
maximal solution. We show that the following simplication rules compute solved
forms for satisable acyclic left-linear systems:
Typing Constraint Logic Programs 15
if K  K 0 and
if  62 V ,  62 V (l) for any l  r 2 , and  62 V (Max( )).
Lemma 4.1
The rules terminate in O(n) steps, where n is the sum of the sizes of the terms in
the left-hand side of inequalities.
Proof
It su-ces to remark that each rule strictly decreases the sum of the size of the terms
in the left-hand sides of the inequalities: (Triv) and (VarLeft) by one, (Decomp) by
at least one, and (VarRight) by the size of  .
One can easily check that each rule preserves the left-linearity as well as the
acyclicity of the system, moreover:
Lemma 4.2
Each rule preserves the satisability of the system, as well as its maximal solution
if one exists.
Proof
Rules (Decomp) and (Triv) preserve all solutions, by denition of the subtyping
order. Rule (VarLeft) replaces a parameter  by its upper bound  . As the system is
left-linear this computes the maximal solution for , and thus preserves the maximal
solution of the system if one exists. Rule (VarRight) replaces a parameter  having
no occurrence in the left-hand side of an inequality, hence having no upper bound,
by the maximum type of its lower bound  ; this computes the maximal solution for
, and thus preserves also the maximal solution of the system if one exists.
Theorem 4.1
Let  be an acyclic left-linear system. Let  0 be a normal form of . Then  is
is in solved form, in which case  0 is a maximal solution of .
Proof
Consider a normal form  0 for . If  0 contains a non variable pair    0 , as this
inequality is irreducible by (Decomp)  0 has no solution, hence  is unsatisable
by lemma 4.2. Similarly  0 has no solution if it contains an inequality    with
(prop. 2.5) or an inequality    with  2 V (Max())
and  6=  (Prop. 2.5). In the other cases, by irreducibility and by acyclicity,  0
contains no inequality, hence  0 contains only equalities that are in solved form,
and the substitution associated to  0 is a maximal solution for .
Francois Fages and Emmanuel Coquery
4.2 The general case
In absence of subtype relations between type constructors of dierent arities, checking
the consistency of general subtype inequalities in nite types has been shown
by Frey (Frey, 1997) Pspace-complete in an arbitrary poset, with a generalization
of Fuh & Mishra's algorithm
It is an open problem whether the technique used by Frey for proving consistency
in arbitrary posets can be generalized to our case with subtype relations between
type constructors of dierent arities.
If we assume however that the subtyping relation is a lattice, it has been shown by
Pottier (Pottier, 2000a) that the satisability of subtype inequalities can be checked
in cubic time in the structure of innite regular trees, i.e. recursive types (Amadio &
Cardelli, 1993). Note that recursive types admit solutions to equations of the form
list(), namely the type list(list(:::)). Below we present Pottier's algorithm
by a set of simplication rules, and show that in acyclic systems the solving of
subtype constraints on innite types is equivalent to the solving on
nite types.
We assume that the structure of type constructors (K; ) is a lattice with ?
and > types. We maintain our previous assumption on decreasing arities, except
on ? which is below all (n-ary) type constructors. We also assume that if
that is greatest
lower bounds do not introduce new parameters. Similarly, if K 00
then range( K;K 00 Note that there is no loss of generality
with this assumption as the lattice of type constructors can always be completed
by introducing glb and lub constructors with the right number of parameters.
We consider systems of subtype inequalities between parameters of
at types,
that is of the form   ,
at types
can be represented in this form by introducing new parameters and inequalities
between these parameters and the type they represent.
For the sake of presentation, we assume that the initial system to be solved,
rst completed by introducing new variables
S and - S
for each non empty subset S of V 0 , and by adding the inequalities
S   and
- S for all variables  2 S. We also assume that the system is completed
by adding the inequality    for each variable . Given a system  and a set
of variables S we dene the variable
f2V0 j92S 2g and similarly
. The simplication rules are the following:
Typing Constraint Logic Programs 17
if
62  and  6=
if K  K 0 ,
g.
l
if K 00 6= K or  0 6  [ f  g
where K
l
if K 00
where K
Rule (Trans) computes the transitive closure of inequalities between parameters
and is mainly responsible for the cubic time complexity. Rule (Clash) checks the
consistency of the lower and upper bounds of parameters. Rule (Dec) decomposes
at types. These three simple rules are in fact su-cient for checking the satisability
of the system (Pottier, 2000a).
Rules (Glb) and (Lub) make explicit the greatest and the least solution of the
system by computing the greatest lower bound of upper bounds of parameters and
the least upper bound of their lower bounds. We remark that if the algorithm is
applied to an initial system  containing a unique inequality of the form
and    0 for each parameter , the algorithm maintains unique upper and lower
bounds for each parameter. We note lb() (resp. ub()) the lower (resp. upper)
bound of  in the system in irreducible form.
Proposition 4.1
The rules terminate.
Proof
Termination with rule (Clash) is trivial. For the other rules, let us consider, as
complexity measure of the system, the couple of integers (t; e) ordered by lexicographic
ordering, where e, the \entropy" of the system, is the number v 2 n, where
Francois Fages and Emmanuel Coquery
v is the number of parameters in the system, n is the number of inequalities between
parameters, and where t, the \temperature" of the system, is the sum of the
height of constructors at the right of , and of the depth of constructors at the left
of . The height (resp. depth) of a constructor is the length of the longest path
of the constructor to ? (resp. >) in (K; ). We show that no rule increases the
temperature of the system, and each rule either decreases t or e.
Rule (Trans) does not change t and decreases e by 1, Rule (Dec) does not change t
and decreases e by at least 1, Rules (Glb) either decreases t if K 00 6= K 0 or decreases
e otherwise, and similarly for rule (Lub). Hence the algorithm terminates.
Theorem 4.2
(Pottier, 2000a) A system of inequalities is satisable over innite regular trees if
and only if the simplication rules do not generate false, in which case the identi-
cation of all parameters to their upper bound ub() (resp. their lower bound lb())
provides a maximum (resp. minimum) solution.
Furthermore, one can show that in our setting of acyclic systems and covariant
constructor types, the solving of subtype constraints on innite types is equivalent
to the solving on nite types.
Theorem 4.3
An acyclic system of inequalities is satisable over nite types if and only if the
simplication rules do not generate false, in which case the identication of all
parameters to their upper bound (resp. lower bound) provides a maximum (resp.
Proof
It is su-cient to remark that the simplication rules preserve the acyclicity of the
system, and that in an acyclic system, the identication of the parameters to their
bounds creates nite solutions.
Corollary 4.1
In a lattice structure without ?, an acyclic system of inequalities is satisable
over nite types if and only if the simplication rules do not generate false and
parameters .
5 Type inference
As usual with a prescriptive type system, type reconstruction algorithms can be
used to omit type declarations in programs, and still check the typability of the program
by the possibility or not to infer the omitted types (Lakshman & Reddy, 1991)
. Below we describe algorithms for inferring the type of variables and predicates,
assuming type declarations for function symbols.
5.1 Type inference for variables
Types for variables in CLP clauses and queries can be inferred by introducing
unknowns for their type in the variable typing, and by collecting the subtype in-
Typing Constraint Logic Programs 19
equalities along the derivation of the type judgement just like in the type checking
algorithm.
It is easy to check that the system of subtype inequalities thus collected is still
acyclic, as the unknown types for CLP variables appear only in left positions. The
system is however not left-linear if a CLP variable has more than one occurrence
in a clause or a query.
The second algorithm of the previous section can thus be used to infer the type
of variables in CLP clauses and queries.
5.2 Type inference for predicates
Types for predicates can be inferred as well under the assumption that predicates
are used monomorphically inside their (mutually recursive) denition (Lakshman
Reddy, 1991). This means that inside a group of mutually recursive clauses, each
occurrence (even in the body of a clause) of a predicate dened in these clauses
must be typed with rule Head instead of rule Atom. The reason for this restriction,
similar to the one done for inferring the type of mutually recursive functions in
ML, is to avoid having to solve a semi-unication problem: i.e. given a system of
types
substitution  such that for all i there exists
a substitution  i s.t.  i
i , that is proved undecidable in (Kfoury et al.,
1989).
Note that the SSI obtained by collecting the subtype inequalities in the derivation
of typing judgements is still acyclic, as the unknown types for predicates appear
only in the right-hand sides of the inequalities. The second algorithm of the previous
section can thus be used also to infer the type of predicates in CLP programs under
the assumption that the structure of types is a lattice without ?.
One consequence of the acyclicity of the system however, is that the maximum
type of a predicate is always >. Indeed in our type system a predicate can always
be typed as maximally permissive. In the more general structure of posets with
suprema, unless the unknown types for predicates are compared with types belonging
to dierent -connected components (in which case the predicate is not
typable), the substitution of an unknown type by the root of its -connected component
is always a solution. But in all cases, this is obviously not a very informative
type to infer.
Our strategy is to infer two types for predicates: the minimum type of the predicate
and a heuristic type. The type inference algorithm proceeds as follows:
Firstly, the minimum type of the predicate is obtained by computing the minimum
solution of the SSI associated to the typing of the complete denition
of the predicate. The minimum type of the ith argument of the predicate
is the type  is the unknown type associated to the ith
argument of the predicate in the SSI. This minimum type is a lower bound of
all possible typings of the predicate.
Secondly, the heuristic type is computed. This type can be parametric. It is
computed in two steps:
Francois Fages and Emmanuel Coquery
| First a heuristic upper type is computed for the predicate. The heuristic
upper type  i of the ith argument of the predicate is obtained by collecting
the upper types fub(X1 ); :::; ub(Xn )g of all the variables fX 1 ; :::;
which occur in the ith position of the predicate in its denining clauses.
be the greatest lower bound of the types
of the variable arguments. We set
if the identication  creates a cycle,
| Then the heuristic type is computed by inferring a possibly parametric
type from the SSI associated to the heuristic upper type. The candidates
for parametric types are the parameters bounded by ? and > in the SSI
associated to the heuristic upper type. Each candidate is checked iteratively
by replacing it with a new constant and by identifying all parameters
which have the new constant in one of their bounds.
Although tedious, one can easily check that the conditions imposed in the de-
nition of the heuristic type create sound typings. The heuristic types thus provide
correct type declarations for type checking the program.
6 Implementation of the type system
6.1 The Wallace library for solving subtype inequalities
Our current implementation uses the Wallace library by F.Pottier (Pottier, 2000b)
for solving the subtype inequalities for type inference and type checking. In both
cases, the set of type constructors (K; ) has thus to be a lattice as described in
section 4. Note that the type system did not require that condition:  could be any
arity decreasing order relation on K.
As required in the type inference algorithm, the > element is distinguished from
the type term which stands for all Prolog terms. The type ? is not considered as a
valid typing as it is an empty type.
Note that the Wallace library authorizes constrained type schemes, like for example
oat !, which expresses the resulting type of + as a function of
the type of its arguments. For the sake of simplicity, we do not consider constrained
type schemes in this paper.
6.2 The type checker
The type checker rst reads the Prolog les and deduces the les containing type
information to load. There is one le for each Prolog le source plus one le for
each module used (as :- use_module(somemodule) in Sicstus Prolog). The system
then loads the type les and builds the structure of type constructors.
The type checker does not impose to give the type of CLP variables in clauses
Typing Constraint Logic Programs 21
and queries. Instead the type of variables is inferred as described in section 5. The
environment U is built with type unknowns for variables. The subtype inequality
system is collected by applying the rules of the type system and at each step,
Wallace is used to solve the type constraints.
One di-culty appears for checking the denitional genericity condition. A type
error must be raised when the denition of a predicate uses, as argument of the
head of the clause, a term whose type  is a subtype of an instance of the declared
type  0 for this argument, and not just of a renaming. But Wallace is not able to
make the dierence between being a subtype of an instance or of a renaming of a
type  0 . The following consideration allows us to work around this di-culty. If
is a subtype of a renaming of  0 , for all instances  0  0 of  0 there must exist an
instance  of  such that    0  0 . For checking denitional genericity, we thus
replace each parameter  appearing in the declared type of the head predicate by
a constructor  , that does not appear in the program, and such that :
term, and  6  for all constructor ,  6=  ,  6= term
If the rule (Atom) can be applied, using the transformed type, then the rule
(Head) can be applied as well with the original type.
6.3 Type inference for predicates
As described in section 5, two types are infered for predicates: a minimum type
which is a lower bound of all possible typings of the predicate, and a heuristic type
which may be parametric.
If type inference is just displayed for user information, we print both types. If it
is used for typing automatically the program in a non-interactive manner, then we
choose the heuristic bound, since it is the most permissive type.
7 Experimental results
7.1 Detection of programming errors
Here we show a small catalog of the kind of programming errors detected by the
type checker.
7.1.1 Inversion of arguments in a predicate or a function
This error can be detected when, for example, a variable occurs in two positions
that have incompatible types.
Example 7.1
Consider the following clause where the arguments of the length predicate have
been reversed.
22 Francois Fages and Emmanuel Coquery
with the usual declarations :
pred
pred
By the rule (Atom'), the variable L3 must be of both types list() and int. In
the type hierarchy we use, there is no type smaller than list and int. The subtype
inequalities in the premise of rule (Atom') are thus unsatisable and a type error
is raised.
Note that this example motivates the discard of type
would be detected on variables, since the empty type ? could always be inferred
for the type of any variable.
7.1.2 Misuse of a predicate or a function
This error is detected when a term of a type  appears as an argument of a predicate,
or of a functor that expects an argument of type  0 , but  6  0  for any substitution
.
Example 7.2
Consider the following clause :
declarations:
int for integer division,
pred .
We try to use a
oat (3.5) where an int is expected. The rule (Atom') does not
apply.
This kind of error can be detected also inside call to foreign predicates, through
the Prolog interface with the C programming language for example.
Example 7.3
Consider the declaration of a predicate p dened in C using the Sicstus - C interface :
Such a declaration is interpreted as a type declaration for
pred
Then a call in a program such as :
:- p(3.14).
raises a type error since the argument is a f loat and the predicate expects an int.
Typing Constraint Logic Programs 23
7.1.3 Wrong predicate denition w.r.t. the declared type
This error is detected by two ways, corresponding to the two preceding kinds of
errors. In the two following examples, the predicate p has been declared with type
pred .
Example 7.4
Let p be dened by p([]).
Here the term [] is used as an argument of p, which requires that p accepts arguments
of type atomic list. But atomic list 6 int and the rule (Atom') does not
apply.
Example 7.5
Let p be dened by :
pred
In this case, we will infer a type for X that must be smaller than list() (using
rule (Atom'), because X is used by length) and smaller than int (using the rule
(Head')). As before, these types have no common subtypes, and an error is raised.
7.1.4 Violation of the denitional genericity condition
Example 7.6
p([1]).
pred
Although the argument of p is a list, but its type is list(int), an instance and not
a renaming of list() (because int 6  ).
This error can also be detected when a variable is in the head of the clause :
Example 7.7
pred
The variable X must be of type f loat and  . The only common subtype is ? and
an error is raised.
Francois Fages and Emmanuel Coquery
7.2 Type checked programs
To test our system, we rst tried it on 20 libraries of Sicstus Prolog, that is around
predicates. Then we type checked an implementation of CLP(FD) written completely
in Prolog, using a lot of meta-predicates, that contains around 170 predi-
cates. These tests where done using type declarations for around 100 built-in ISO
Prolog predicates and for some more built-in Sicstus predicates.
Some type errors obtained in the libraries came from the overloading of some
function symbols. For example, the function '-'/2 is used for coding pairs as well as
for coding the arithmetic operation over numbers. Another example of overloading
comes from options : it happens that some terms are common to two sets of options,
of types  1 ,  2 . In this case, it is enough to create a subtype  of both  1 and  2 ,
and tell that the common terms are of type  .
We also skip the type checking of some particular declarations, such as mode
declarations (which are not used by our type system) :
Example 7.8
:- mode p(+,-,+) , q(-,?).
These declarations can be typed in another type structure for mode declarations,
but not in the same type structure as the one for predicates, since the predicate
are clearly overloaded in such declarations.
7.3 Type inference for predicates
As said in section (6.3), we infer an interval of types for predicates. Both bounds
of the interval may oer interesting information.
Example 7.9
append([Head| Tail], List, [Head| Rest]) :-
append(Tail, List, Rest).
append([], List, List).
Minimum type: list(bottom), list(bottom), list(bottom) -> pred
Heuristic infered type: list(A), list(A), list(A) -> pred
Example 7.10
sum_list([], Sum, Sum).
sum_list([Head| Tail], Sum0, Sum) :-
Sum1 is Head+Sum0, sum_list(Tail, Sum1, Sum).
Minimum type: list(bottom), bottom, bottom -> pred
Heuristic infered type: list(float), float, float -> pred
Sometimes, the heuristic infers a too permissive type. This is in particular the
case with overloaded arithmetic predicates expressions, that are always typed as
float, not int.
Typing Constraint Logic Programs 25
Example 7.11
length([],0).
length([_|Tail],R) :- length(Tail, L), R is L+1.
Minimum type: list(bottom), int -> pred
Heuristic infered type: list(A), float -> pred
The heuristic may also infer a type which is too restrictive.
Example 7.12
is_list([]).
Minimum type: list(bottom) -> pred
Heuristic infered type: list(A) -> pred
This is a typical example where the maximum type, here
pred
is in fact the intended type.
These examples should clearly justify the heuristic approach to type inference for
predicates in a prescriptive type system.
Finally, the interesting f latten predicate illustrates the remarkable
exibility of
the type system.
Example 7.13
pred
pred
7.4 Benchmarks
The following table sums up our evaluation results. The rst column indicates
the type checked Prolog program les. The second column indicates the number
of predicates dened in each le rst, and then the maximum number of atoms
by clause and by complete connected component. The third column indicates the
time in seconds for type checking the program with the type declarations for
function and predicate symbols. The fourth column indicates the CPU for inferring
the types of predicates with the type declarations for function symbols only. The
last column indicates the percentage of predicates for which the infered type is
exactly the intended type.
The last test le is another implementation of CLP(FD) on top of prolog which
uses a lot of metaprogramming predicates.
26 Francois Fages and Emmanuel Coquery
File # predicates Type Checking Type Inference % exact types
assoc.pl
bdb.pl 101 27/27 23.56 s 41.10 s 64 %
charsio.pl 15 7/7 1.27 s 2.21 s 33 %
clpb.pl 59 20/77 24.35 s 1827.32 s n/a
clpq 396 39/160 355.12 s 4034.37 s n/a
clpr 439 39/160 304.45 s 3958.41 s n/a
jasper.pl
lists.pl
random.pl 11
sockets.pl
ugraphs.pl 87 12/24 48.21 s 274.22 s 67 %
clp-fd.pl 163 20/71 24.35 s 59.65 s n/a

Table

3. Benchmarks.
The same algorithm is used for solving the systems of subtype inequalities for
type checking and type inference. The dierence between computation times comes
from the handling of complete connected components of denitions for type infer-
ence, whereas for type checking, clauses are type checked one by one. In particular
CLP(R) and CLP(Q) have very large mutually recursive clauses.
In the library for arrays, the low percentage of exact matches between the infered
type and the intended type is simply due to the typing of indices by
oat instead
of int. The errors in the other libraries are also due to the typing of arithmetic
expressions by
oat , and sometimes to the use of the equality predicate = ; which
creates a typing by term for some arguments instead of a more restrictive typing.
In the library CLP(FD), nite domain variables are typed with type int. Similarly
in the library CLP(R), variables over the reals are typed with type
oat .
One consequence is that the type checker then allows coercions from nite domain
variables to real constraint variables. To make these coercions work in practice one
modication in the CLP(R) library was necessary.
8 Conclusion
Typing constraint logic programs for checking programming errors statically while
retaining the
exibility required for preserving all the metaprogramming facilities
Typing Constraint Logic Programs 27
of logic programming and the usual coercions of constraint programming, is the
challenge that conducted the design of the type system presented in this paper. Our
experiments with the libraries of Sicstus Prolog have shown that the type system
is simple and
exible enough to accept a large variety of constraint logic programs.
The main di-culties are located to con
icts of overloading for some predicates or
functions. Such ad hoc polymorphism could be resolved by considering disjunctive
formula over types (Demoen et al., 1999). Examples have been given also to show
that the type system is useful enough for detecting programming errors such as the
inversion of arguments in a predicate, or the unintended use of a predicate.
The price to pay for this
exibility is that our type system may be regarded
as too permissive. Some intuitively ill-typed queries may be not rejected by the
type system. We have analyzed these defects in terms of the subject reduction
properties of the type system. In particular we have shown that the addition of the
typing constraints on variables to well-typed programs and queries su-ces to state
subject reduction w.r.t. both CSLD resolution and substitution steps, and has for
eect to reject a larger set of clauses and queries by checking the satisability of
their constraints with the type constraints at compile-time.
The lattice assumption for the type structure, due to the implementation in Wallace
of subtype constraints, may be regarded also as too demanding in some cases.
We have already relaxed that assumption by rejecting the bottom element from
the structure of types. Nevertheless the decidability of subtype constraints under
more general assumptions is an interesting open problem. In particular, whether
the method of Frey (Frey, 1997) can be extended to cover subtype relations between
type constructors of dierent arities, as required in our approach, is an open
question.
Finally, it is worth noting that the results presented here are not limited to logic
programming languages. They should be relevant to various constraint programming
languages, where the main di-culty is to type check constraint variables, that
express the communication between dierent constraint domains.

Acknowledgment

. We would like to acknowledge fruitful discussions with Francois
Pottier, Didier Remy, Jan Smaus and Alexandre Frey on this work. We are also
grateful to the referees for their peer reviews.



--R

Login: A logical programming language with built-in inheritance

Subtyping recursive types.
Type inferencing for polymorphic order-sorted logic programs
Equations and inequalitions on


http://pauillac.

A polymorphic type system with subtypes for Prolog.
Pages 79-93 of: Ganzinger


Satisfying subtype inequalities in polynomial space.
Type inference with subtypes.
Logic programming with type speci

A semantics for typed logic programs.
In (Pfenning


Typed Prolog: A semantic reconstruction of the Mycroft-O'Keefe type system
Type checking and type inferencing for logic programs with subtypes and parametric polymorphism.
A polymorphic type system for prolog.
Types in logic programming.


Using modes to ensure subject reduction for typed logic programs with subtyping.
Logic programming with polymorphically order-sorted types
Logic programming over polymorphically order-sorted types


Subtype inequalities.

In (Pfenning
--TR

--CTR
Adam Kiezun , Michael D. Ernst , Frank Tip , Robert M. Fuhrer, Refactoring for Parameterizing Java Classes, Proceedings of the 29th International Conference on Software Engineering, p.437-446, May 20-26, 2007
Wodzimierz Drabent , Jan Mauszyski , Pawe Pietrzak, Using parametric set constraints for locating errors in CLP programs, Theory and Practice of Logic Programming, v.2 n.4-5, p.549-610, July 2002
metaprogramming;type systems;prolog;constraint logic programming;subtyping