Data Type Inference for Logic Programming

Abstract

In this paper we present a new static data type inference algorithm for logic programming. Without the need for declaring types for predicates, our algorithm is able to automatically assign types to predicates which, in most cases, correspond to the data types processed by their intended meaning. The algorithm is also able to infer types given data type definitions similar to data definitions in Haskell and, in this case, the inferred types are more informative, in general. We present the type inference algorithm, prove it is decidable and sound with respect to a type system, and, finally, we evaluate our approach on example programs that deal with different data structures.

1 Introduction

Types are program annotations that provide information about data usage and program execution. Ensuring that all types are correct and consistent may be a daunting task for humans. However, this task can be automatized with the use of a type inference algorithm which assigns types to programs.

Logic programming implementers have been interested in types from early on [Zob87, DZ92, Lu01, FSVY91, YFS92, MO84, LR91, SBG08, HJ92, SCWD08]. Most research approached typing as an over-approximation (a superset) of the program semantics [Zob87, DZ92, YFS92, BJ88, FSVY91]: any programs that succeed will necessarily be well-typed. Other researchers followed the experience of functional languages and took a more aggressive approach to typing, where only well-typed programs are acceptable [MO84, LR91]. Over the course of the last few years it has become clear that there is a need for a type inference system that can support Prolog well [SCWD08]. Next, we report on recent progress on our design, the $YAP^T$ type system¹. We will introduce the key ideas and then focus on the practical aspects.

Our approach is motivated by the belief that programs (Prolog or otherwise) are about manipulating data structures. In Prolog, data structures are denoted by terms with a common structure and, being untyped, one cannot naturally distinguish between failure and results of type erroneous calls. We believe that to fully use data structures we must be able to discriminate between failure, error, and success. Thus our starting point was a three-valued semantics that clearly distinguishes type errors from falsehood [BFC19].

There, we first define the $YAP^T$ type system that relates programs with their types. This defines the notion of well-typed program as a program which is related to a type by the relation defined by the type system. Here we present the $YAP^T$ type inference algorithm which is able to automatically infer data type definitions. Finally we show that our type inference algorithm is sound with respect to the type system, in the sense that the inferred type for a program makes the program well-typed.

We shall assume that typed Prolog programs operate in a context, e.g., suppose a programming context where the well-known append predicate is expected to operate on lists:

This information is not achievable when using type inference as a conservative approximation of the success set of the predicate. The following figure shows the output of type inference in this case, where ti is the type of the i-th argument of append, “+” means type disjunction and “A” and “B” are type variables (Fig. 1):

Fig. 1.

(1) Program approximation; (2) Well-typing

Types t2 and t3, for the second and third argument of the left-hand side (1), do not filter any possible term, since they have a type variable as a member of the type definition, which can be instantiated with any type. And, in fact, assuming the specific context of using append as list concatenation, some calls to append succeed even if unintended², such as append([],1,1). The solution we found for these arguably over-general types is the definition of closed types, that we first presented in [BFSC17], which are types where every occurrence of a type variable is constrained. We also defined a closure operation, from open types into closed types, using only information provided by the syntax of the programs themselves. Applying our type inference algorithm with closure to the append predicate yields the types on the right-hand side (2), which are the intended types [Nai92] for the append predicate.

Our type inference algorithm³ works for pure Prolog with system predicates for arithmetic. We assume as base types int, float, string, and atom. There is an optional definition of type declarations (like data declarations in Haskell) which, if declared by the programmer, are used by the type inference algorithm to refine types. We follow a syntax inspired in [SCWD08] to specify type information. One example of such a declaration is the list datatype

:- type list(A) = [] + [A | list(A)].

In order to simplify further processing our type system and type inference algorithm assume that predicates are in a simplified form called kernel Prolog [VR90]. In this representation, each predicate in the program is defined by a single clause (H :- B), where the head H contains distinct variables as arguments and the body B is a disjunction (represented by the symbol ; ) of queries. The variables in the head of the clause occur in every query in the body of that clause. We assume that there are no other common variables between queries, except for the variables that occur in the head of the clause, without loss of generality. In this form the scope of variables is not limited to a single clause, but is extended over the whole predicate definition and thus type inference is easier to perform. In [VR90] a compilation from full Prolog to kernel Prolog is defined. Thus, in the rest of the paper, we will assume that predicate definitions are always in kernel Prolog.

2 Types

Here we define a new class of expressions, which we shall call types. We first define the notion of type term built from an infinite set of type variables TVar, a finite set of base types TBase, an infinite set of constants TCons, an infinite set of function symbols TFunc, and an infinite set of type symbols, TSymb. Type terms can be:

• a type variable ($\alpha ,\beta ,\gamma ,\dots \in TVar$)

• a constant ($1, [~], `c\text {'},\dots \in TCons$)

• a base type ($int, float, \dots \in TBase$)

• a function symbol $f \in TFunc$ associated with an arity n applied to an n-tuple of type terms (f(int, [ ], g(X)))

• a type symbol $\sigma \in TSymb$ associated with an arity n ($n \ge 0)$ applied to an n-tuple of type terms ($\sigma (X,int)$).

Type variables, constants and base types are called basic types. A ground type term is a type variable-free type term. Type symbols can be defined in a type definition. Type definitions are of the form:

$$\sigma (\alpha _1,\ldots ,\alpha _k) = \tau _1 + \dots + \tau _n,$$

where each $\tau _i$ is a type term and $\sigma$ is the type symbol being defined. In general these definitions are polymorphic, which means that type variables $\alpha _1,\ldots ,\alpha _k$, for $k \ge 0$, include the type variables occurring in $\tau _1 + \dots + \tau _n$, and are called type parameters. If we instantiate one of those type variables, we can replace it in the parameters and everywhere it appears on the right-hand side of the definition. The sum $\tau _1 + \dots + \tau _n$ is a union type, describing values that may have one of the types $\tau _1,\ldots ,\tau _n$. The ‘+’ is an idempotent, commutative, and associative operation. Throughout the paper, to condense notation, we will use the symbol $\bar{\tau }$ to denote union types. We will also use the notation $\tau \in \bar{\tau }$ to denote that $\tau$ is a summand in the union type $\bar{\tau }$.

Note that type definitions may be recursive. A deterministic type definitions is a type definition where, on the right-hand side, none of $\tau _i$ start with a type symbol and if $\tau _i$ is a type term starting with a function symbol f, then no other $\tau _j$ starts with f.

Example 1

Assuming a base type int for the set of all integers, the type list of integers is defined by the type definition $list = [~] + [int~|~list]$⁴.

Let $\overrightarrow{\tau }$ stand for a tuple of types $\tau _1 \times \dots \times \tau _n$. A functional type is a type of the form $\overrightarrow{\tau _1} \rightarrow \tau _2$. A predicate type is a functional type from a tuple of the type terms defining the types of its arguments to bool, i.e. $\tau _1 \times \ldots \times \tau _n \rightarrow bool$. A type can be a type term, an union type, or a predicate type.

Our type language enables parametric polymorphism through the use of type schemes. A type scheme is defined as $\forall _{X_1}\ldots \forall _{X_n} T$, where T is a predicate type and $X_1,\ldots ,X_n$ are distinct type variables. In logic programming, there have been several authors that have dealt with polymorphism with type schemes or in a similar way [PR89, BG92, Hen93, Zob87, FSVY91, GdW94, YFS92, FD92, Han89]. Type schemes have type variables as generic place-holders for ground type terms. Parametric polymorphism comes from the fact these type variables can be instantiated with any type.

Example 2

A polymorphic list is defined by the following type definition:

$$list(X) = [~] + [X~|~list(X)]$$

Notation. Throughout the rest of the paper, for the sake of readability, we will omit the universal quantifiers on type schemes and the type parameters as explicit arguments of type symbols in inferred types. Thus we will assume that all free type variables on type definitions of inferred types are type parameters which are universally quantified.

Most type languages in logic programming use tuple distributive closures of types. The notion of tuple distributivity was given by Mishra [Mis84]. Throughout this paper, we restrict our type definitions to be deterministic. The types described this way are tuple distributive.

Sometimes, the programmer wants to introduce a new type in a program, so that it is recognized when performing type inference. It is also a way of having a more structured and clear program. These declarations act similarly to data declarations in Haskell.

In our algorithm, types can be declared by the programmer in the following way:- $\texttt {type}~type\_symbol(type\_vars) = type\_term_1 + \dots + type\_term_n$. One example would be:

In the rest of the paper we will assume that all constants and function symbols that start a summand in a declared type cannot start a summand in a different one, thus there are no overloaded constants nor function symbols. Note that there is a similar restriction on data declarations in functional programming languages.

2.1 Semantics

In [BFC19] we defined a formal semantics for types. Here we just give the main intuitive ideas behind it:

• The semantics of base types and constant types are predefined sets containing logic terms, for instance, the base type int is the set of all integers and the semantics of bool is the set of the values true and false;

• Tuples of types, $(\tau _1,\dots ,\tau _n)$, are sets of tuples of terms such that the semantics of each term belongs to the semantics of the type in the corresponding position;

• $f(\tau _1,\dots ,\tau _n)$ is the set of all terms with main functor f and arity n applied to the set of tuples belonging to the semantics of $(\tau _1,\dots ,\tau _n)$;

• The semantics of union types is the disjoint union of the semantics of its summands;

• The semantics of type symbols is the set of all terms that can be derived from its definition;

• The semantics of functional types, such as predicate types, is the set of functions that when given terms belonging to the semantics of the input types, output terms belonging to the semantics of output types. For instance the semantics of $int \times float \rightarrow bool$, contains all functions that, given a pair with an integer and a floating point number, output a boolean.

• The semantics of parametric polymorphic types is the intersection of the semantics of its instances (this idea was first used by Damas [Dam84] to define the semantics of type schemes).

In [BFC19] we defined a type system and proved that it is sound with respect to this semantics of types. Here we define a type inference algorithm and prove that it is sound with respect to the type system, thus, using these two results, we can conclude that the type inference algorithm is also sound with respect to the semantics.

2.2 Closed Types

Closed types were first defined in [BFSC17]. Informally, they are types where every occurrence of a type variable is constrained. If a type is not closed, we say that it is an open type. The restrictions under the definition of closed type can be compressed in the following three principles:

• Types should denote a set of terms which is strictly smaller than the set of all terms

• Every use of a variable in a program should be type constrained

• Types are based on self-contained definitions.

The last one is important to create a way to go from open types to closed types. We defined what is an unconstrained type variable as follows:

Definition 1 (Unconstrained Type Variable)

A type variable $\alpha$ is unconstrained with respect to a set of type definitions T, notation unconstrained$(\alpha ,T)$, if and only if it occurs exactly once as a summand in the set of all the right-hand sides of type definitions in T.

Unconstrained type variables type terms with any type, thus they do not really provide type information. We now define closed type definition, which are type definitions without type variables as summands in their definition.

Definition 2 (Closed Type Definitions)

A type definition $\sigma = \bar{\tau }$ is closed, notation closedTypeDef$(\sigma )$, if and only if there are no type variables as summands in $\bar{\tau }$.

The definition for closed types uses these two previous auxiliary definitions. Closed types correspond to closed records or data definitions in functional programming languages. The definition follows:

Definition 3 (Closed Types)

A type definition $\sigma = \bar{\tau }$ is closed with respect to a set of type definitions T, notation closed$(\sigma ,T)$, if and only if the predicate defined as follows holds:

$$\begin{aligned} closed(\sigma ,T) = \left\{ {\begin{array}{ll} \lnot unconstrained(\alpha ,T)\;\;\; &{} if\; \bar{\tau } = \alpha \,\, and \,\, \alpha \,\, is\,\, a\,\, type\,\, variable \\ closedTypeDef(\sigma ) &{} otherwise \end{array}}\right. \end{aligned}$$

Example 3

We recall the example in the Introduction, of the following types for the append predicate, where $t_n$ is the type of nth predicate argument:

Type t3, for the third argument of append, is open, because t3 has a type variable as a summand, thus it does not filter any possible term, since the type variable can be instantiated with any type. An example of a valid closed type for append is:

The next step is to transform open types into closed types. Note that some inferred types may be already closed. For the ones that are not, we defined a closure operation, described in detail in [BFSC17]. This closure operation is an optional post-processing step on our algorithm.

To close types, we calculate what we call the proper variable domain of every type variable that occurs as a summand in a type definition. The proper variable domain corresponds to the sum of the proper domains of each type that shares a type term with the open type we are tying to close. The proper domain of a type is the sum of all summands that are not type variables in its definition. We then replace the type variable with its proper variable domain.

We have tested the closure algorithm on several examples and for the examples we tried, the results seem very promising.

3 Examples

There are some flags in the type inference algorithm that can be turned on or off:

• basetype (default: on) - when this flag is turned on, we assume that each constant is typed with a base type, when it is turned off, we type each constant with a constant type corresponding to itself;

• list (default: off) - this flag adds the data type declaration for polymorphic lists to the program when turned on;

• closure (default: off) - when this flag is turned on, the closure operation is applied as a post-processing step on the algorithm.

In the following examples pi is the type symbol for the type of the ith argument of predicate p and we assume that all free type variables on type definitions are universally quantified and that the type of arguments of built-in arithmetic predicates is predefined as $int + float$.

Example 4

Let us consider the predicate concat, which flattens a list of lists, where app is the append predicate:

The types inferred with all the flags off correspond to types inferred in previous type inference algorithms which view types as an approximation of the success set of the program:

Now the types inferred when turning on the closure flag are:

Note that these types are not inferred by any previous type inference algorithm for logic programming so far, and they are a step towards the automatic inference of types for programs used in a specific context, more precisely, a context which corresponds to how it would be used in a programming language with data type declarations, such as Curry [Han13] or Haskell.

Example 5

Let rev be the reverse list predicate, defined using the append definition used in the previous example:

The inferred types with all flags off is (the types inferred for append are the same as the one in the previous example):

If we turn on the list_flag, which declares the data type for Prolog lists, the type inference algorithm outputs the same types that would be inferred in Curry or Haskell with pre-defined built-in lists:

We now show an example of the minimum of a tree.

Example 6

Let $tree\_minimum$ be the predicate defined as follows:

The inferred types with all flags off, except for the $basetype\_flag$, are:

If we now add a predefined declaration of a tree data type and turn on the $list\_flag$, the algorithm outputs:

4 Type System

Here we define the notion of well-typed program using a set of rules assigning types to terms, atoms, queries, sequences of queries, and clauses. This is generally called a type system and ours follows the definition in [BFC19] with some differences in the notation for recursive types: here we explicitly add a set of (possibly recursive) type definitions instead of the fix-point notation for types used in the paper mentioned above. These small differences do not alter the soundness of the type system.

We first write the following subtyping relation from [BFC19].

Definition 4 (Subtyping)

Let $\phi$ be a substitution of types for type variables. Let $\sqsubseteq$ denote the subtyping relation as a partial order (reflexive, anti-symmetric and transitive) defined as follows:

• $\tau \sqsubseteq \tau \prime$ if $\exists \phi . \phi (\tau \prime ) = \tau$ (Instance)

• $\tau \sqsubseteq \bar{\tau }$ iff $\tau \in \bar{\tau }$ (Subset)

• $f(\tau _1,\dots , \tau _n) \sqsubseteq f(\tau \prime _1,\dots ,\tau \prime _n)$ iff $\tau _1\le \tau \prime _1, \dots \tau _n \le \tau \prime _n$ (Complex term construction/destruction)

• $\delta _1 \sqsubseteq \delta _2$ iff, assuming $\delta _1\sqsubseteq \delta _2$, we get $\bar{\tau }_1 \sqsubseteq \bar{\tau }_2$, where $\delta _1 = \bar{\tau }_1$ and $\delta _2 = \bar{\tau }_2$ are the type definitions for $\delta _1$ and $\delta _2$ (Recursive Type Unfolding)

• $\tau \sqsubseteq \delta$ iff $\tau \sqsubseteq \bar{\tau }$ and $\delta = \bar{\tau }$ is the type definition for $\delta$ (Right Unfolding)

• $\delta \sqsubseteq \tau$ iff $\bar{(}\tau )\sqsubseteq \tau$ and $\delta = \bar{\tau }$ is the type definition for $\delta$ (Left Unfolding)

• $\tau \sqsubseteq \tau _1 + \tau _2$ iff $\tau \sqsubseteq \tau _1$ or $\tau _2 \sqsubseteq \tau$ (Addition)

• if $\tau \prime \sqsubseteq \tau$, then $\tau \rightarrow bool \sqsubseteq \tau \prime \rightarrow bool$ (Contravariance)

Subtyping of functional types is contravariant in the argument type, meaning that the order of subtyping is reversed. This is standard in functional languages and guarantees that when a function type is a subtype of another it is safe to use a function of one type in a context that expects a function of a different type. It is safe to substitute a function f for a function g if f accepts a more general type of argument than g. For example, predicates of type $int + float \rightarrow bool$ can be used wherever an $int \rightarrow bool$ was expected.

Let us now give some auxiliary definitions: an assumption is a type declaration for a variable, written $X:\tau$, where X is a variable and $\tau$ a type. We define a context $\varGamma$ as a set of assumptions with distinct variables as subjects (alternatively contexts can be defined as functions from variables to types, where $domain(\varGamma )$ stands for its domain). Since $\varGamma$ can be seen as a function, we use $\varGamma (X) = \tau$ to denote $(X : \tau ) \in \varGamma$. A set of type definitions, $\varDelta$, is a set of type definitions of the form $\sigma = \bar{\tau }$, where each definition has a different type symbol on the left-hand side. It can also be defined as a function from $\sigma$ to $\bar{\tau }$. We will therefore use the notation $\varDelta (\sigma ) = \bar{\tau }$ to denote $(\sigma = \bar{\tau }) \in \varDelta$.

Our type system is defined in Fig. 2 and statically relates well-typed programs with their types by defining a relation $\varGamma ,\varDelta \vdash _{P} p:\tau$, where $\varGamma$ is a context, $\varDelta$ a set of type definitions, p is a term, an atom, a query, a sequence of queries, or a clause, and $\tau$ is a type. This relation should be read as expression p has type $\tau$, given the context $\varGamma$ and type definitions $\varDelta$, in a program P. We will write $\varGamma \cup \{X:\tau \}$ to represent the context that contains all assumptions in $\varGamma$ and the additional assumption $X:\tau$ (note that because each variable is unique as a subject of an assumption in a context, in $\varGamma \cup \{X:\tau \}$, $\varGamma$ does not contain assumptions with X as subject). We will write a sequence of variables $X_1,\dots , X_n$ as $\overrightarrow{X}$, and a sequence of types as $\overrightarrow{\tau }$. We assume that clauses are normalized and, therefore, every call to a predicate in the body of a clause contains only variables.

Fig. 2.

Type System

Note that we have a different rule for recursive clauses and non-recursive clauses. Whenever we have a recursive clause, its type is derived assuming every recursive call has the same type as the head of the clause. This corresponds to the monomorphic restriction described in [Hen93], where the authors prove that if we allow polymorphic recursion, i.e. recursion with different instances of the same polymorphic type, then inference is not decidable.

Also note that the type for a predicate call is a subtype of the type for the clause defining it. This captures the fact that we can call a polymorphic predicate with a type that is an instance of the general type scheme, or if the input type of the predicate is a union type, we can call it with only some of the summands of that union.

5 Type Inference

We have seen how to define the notion of well-typed program using a set of rules which assign types to programs. Here we will present a type inference algorithm which, given an untyped logic program, is able to calculate a type which makes the program well-typed.

Fig. 3.

Type Inference Algorithm Flowchart

Our type inference algorithm is composed of several modules, as described in Fig. 3. On a first step, when consulting programs, we apply term expansion to transform programs into the internal format that the rest of the algorithm expects. Secondly, we have the type inference phase itself, where constraint generation is performed, and a type constraint solver outputs the inferred types for a given program. There is also a simplification step that is performed during inference, to assure that the type definitions are always deterministic and simplified. After this, we either directly run a type pretty printer, or go through closure before printing the types.

Thus the type inference algorithm is composed of four main parts with some auxiliary steps:

• Term expansion

• Constraint generation

• Constraint solving

• Closure (optional).

Without closure or type declarations our algorithm follows a standard approach of types as approximations of the program semantics. Using our algorithm to infer well-typings (which filter program behaviour instead of approximating it) is possible either by using explicit type declarations or by using the closure step. Using one of the latter approaches, instead of the standard one, yields better results as can be seen in the example Sect. 3.

5.1 Stratification

We assume that the input program of our algorithm is stratified. To understand the meaning of stratified programs, let us define the dependency directed graph of a program as the graph that has one node representing each predicate in the program and an edge from q to p for each call from a predicate p to a predicate q.

Definition 5 (Stratified Program)

A stratified program P is such that the dependency directed graph of P has no cycles of size more than one.

This means that our type inference algorithm deals with predicates defined by direct recursion but not with mutual recursion. Note that stratified programs are widely used and characterize a large class of programs which is used in several database and knowledge base systems [Ull88].

5.2 Constraints and Constraint Generation

The type inference algorithm begins by generating type constraints from a logic program which are solved by a constraint solver in a second stage of the algorithm. There are two different kinds of type constraints: equality constraints and subtyping constraints. An equality constraint is of the form $\tau _1 = \tau _2$ and a subtyping constraint is of the form $\bar{\tau _1} \le \bar{\tau _2}$. Ultimately we want to determine if a set of constraints C can be instantiated affirmatively using some substitution S, that substitutes types for type variables. For this we need to consider a notion of constraint satisfaction $S \models C$, in a first order theory with equality [Mah88] and the extra axioms in Definition 4 for subtyping.

Definition 6 (Constraint satisfaction)

Let $\equiv$ mean syntactic type equality and $\sqsubseteq$ the subtyping relation defined in Definition 4. $S \,\models \, C$ is defined as follows:

• 1. $S \,\models \, \tau _1 = \tau _2$ if and only if $S(\tau _1) \equiv S(\tau _2)$;

• 2. $S \,\models \, \bar{\tau _1} \le \bar{\tau _2}$ if and only if $S(\bar{\tau _1}) \sqsubseteq S(\bar{\tau _2})$;

• 3. $S \,\models \, C$ if and only if $S \,\models \, c$ for each constraint $c \in C$.

The constraint generation step of the algorithm will output two sets of constraints, Eq (a set of equality constraints) and Ineq (a set of subtyping constraints), that need to be solved during type inference.

Let us first present two auxiliary functions to combine contexts. Contexts can be obtained from the disjunction, or conjunction, of other contexts. For this we define two auxiliary functions, $\oplus$ and $\otimes$, to define the result of disjunction, or conjunction, respectively, of context. These definitions are used by the constraint generation algorithm. They are defined as follows:

Definition 7

Let $\varGamma _i$ be contexts, and $\varDelta _i$ be disjoint sets of type definitions defining the type symbols in $\varGamma _i$, respectively. Let V be the set of variables that occur in more than one context.

$\oplus \big ((\varGamma _1,\dots , \varGamma _n), (\varDelta _1,\dots , \varDelta _n)\big ) = (\varGamma ,\varDelta )$, where:

$\varGamma (X) = \sigma \prime$, where $\sigma \prime$ is a fresh type symbol, for all $X \in V$, and $\varGamma (X) = \varGamma _i(X)$, for all $X \notin V \wedge X \in domain(\varGamma _i)$;

$\varDelta (\sigma ) = \varGamma _{i_1}(X) + \dots + \varGamma _{i_k}(X)$, for all type symbols $\sigma \notin \varDelta _1 \cup \dots \cup \varDelta _n$, and $\varDelta (\sigma ) = \varDelta _i(\sigma )$, otherwise.

Definition 8

Let $\varGamma _i$ be contexts, and $\varDelta _i$ be disjoint sets of type definitions defining the type symbols in $\varGamma _i$, respectively. Let V be the set of variables that occur in more than one context.

$\otimes \big ( (\varGamma _1,\dots , \varGamma _n), (\varDelta _1,\dots ,\varDelta _n)\big ) = (\varGamma ,\varDelta ,Eq)$, where:

$\varGamma (X) = \sigma \prime$, where $\sigma \prime$ is a fresh type symbol, for all $X \in V$, and $\varGamma (X) = \varGamma _i(X)$, for all $X\notin V \wedge X \in domain(\varGamma _i)$;

$\varDelta (\sigma ) = \alpha$, where $\alpha$ is a fresh type variable, for all type symbols $\sigma \notin \varDelta _1 \cup \dots \cup \varDelta _n$, and $\varDelta (\sigma ) = \varDelta _i(\sigma )$, otherwise;

$Eq = \{\alpha = \varDelta _i(\varGamma _i(X)), \dots , \alpha = \varDelta _j(\varGamma _j(X))\}$, for all fresh $\alpha$, such that $(\sigma \prime = \alpha ) \in \varDelta$, $\varGamma (X) = \sigma \prime$, and $X \in domain(\varGamma _i) \wedge \dots \wedge X \in domain(\varGamma _j)$.

Let P be a term, an atom, a query, a sequence of queries, or a clause. generate(P) is a function that outputs a tuple of the form $(\tau ,\varGamma ,Eq,Ineq,\varDelta )$, where $\tau$ is a type, $\varGamma$ is an context for variables, Eq is a set of equality constraints, Ineq is a set of subtyping constraints, and $\varDelta$ is a set of type definitions. The function generate, which generates the initial type constraints, is defined case by case from the program syntax. Its definition follows:

$generate(P) =$

• $generate(X) = (\alpha ,\{X:\sigma \},\emptyset ,\emptyset ,\{\sigma = \alpha \})$, X is a variable,

  where $\alpha$ is a fresh type variable and $\sigma$ is a fresh type symbol.

• $generate(c) = (basetype(c),\emptyset ,\emptyset ,\emptyset ,\emptyset )$, c is a constant.

• $generate(f(t_1,\dots ,t_n)) = (basetype(f)(\tau _1,\dots ,\tau _n), \varGamma , Eq, \emptyset , \varDelta )$, f is a function symbol,

  where $generate(t_i) = (\tau _i,\varGamma _i,Eq_i,\emptyset ,\varDelta _i)$,

  $(\varGamma ,\varDelta ,Eq\prime ) = \otimes \big ((\varGamma _1, \dots , \varGamma _n), (\varDelta _1, \dots , \varDelta _n)\big )$, and

  $Eq = Eq_1 \cup \dots \cup Eq_n \cup Eq\prime$.

• $generate(t_1 = t_2) = (bool, \varGamma , Eq, \emptyset ,\varDelta )$

  where $generate(ti) = (\tau _i,\varGamma _i, Eq_i, \emptyset ,\varDelta _i)$,

  $(\varGamma ,\varDelta ,Eq\prime ) = \otimes \big ((\varGamma _1, \varGamma _2), (\varDelta _1, \varDelta _2)\big )$, and

  $Eq = Eq_1 \cup Eq_2 \cup \{\tau _1 = \tau _2\} \cup Eq\prime$.

• $generate(p(X_1,\dots ,X_n)) = (bool, (\{X_1:\sigma _1, \dots , X_n : \sigma _n\}, \emptyset , \{\sigma _1 \le \tau _1, \dots , \sigma _n \le \tau _n\},\varDelta \prime )$, p is a predicate symbol,

  where $generate(p(Y_1,\dots ,Y_n) :- body) = (bool, \varGamma , Eq, Ineq,\varDelta )$,

  $\{Y_1 : \tau _1, \dots Y_n : \tau _n\} \in \varGamma$

  $\varDelta \prime = \varDelta \cup \{\sigma _i = \alpha _i\}$, and $\sigma _i$ and $\alpha _i$ are all fresh.

• $generate(c_1,\dots ,c_n) = (bool, \varGamma , Eq , Ineq_1 \cup \dots \cup Ineq_n,\varDelta )$, a query,

  where $generate(c_i) = (bool,\varGamma _i,Eq_i,Ineq_i,\varDelta _i)$,

  $(\varGamma ,\varDelta ,Eq\prime ) = \otimes \big ( (\varGamma _1, \dots , \varGamma _n), (\varDelta _1, \dots , \varDelta _n)\big )$, and

  $Eq = Eq_1 \cup \dots \cup Eq_n \cup Eq\prime$.

• $generate(b_1;\dots ;b_n) = (bool,\varGamma , Eq_1 \cup \dots \cup Eq_n, Ineq_1 \cup \dots \cup Ineq_n,\varDelta )$,

  where $generate(c_i) = (bool,\varGamma _i,Eq_i,Ineq_i,\varDelta _i)$, and

  $(\varGamma ,\varDelta ) = \oplus \big ( (\varGamma _1,\dots , \varGamma _n), (\varDelta _1, \dots , \varDelta _n)\big )$.

• $generate(p(X_1,\dots ,X_n) :- body.) = (bool, \varGamma , Eq, Ineq, \varDelta )$, a non-recursive clause,

  where $generate(body) = (bool, \varGamma , Eq, Ineq, \varDelta )$.

• $generate(p(X_1,\dots ,X_n) :- body) = (bool, \varGamma , Eq, Ineq\prime , \varDelta )$, a recursive clause,

  where $generate(p(X_1,\dots ,X_n):- body\prime ) = (bool, \varGamma , Eq, Ineq, \varDelta )$, such that $body\prime$ is body after removing all recursive calls,

  and $Ineq\prime = Ineq \cup \{\overrightarrow{\sigma _1} \le \overrightarrow{\tau }, \dots , \overrightarrow{\sigma _k} \le \overrightarrow{\tau }, \overrightarrow{\tau } \le \overrightarrow{\sigma _1}, \dots , \overrightarrow{\tau } \le \overrightarrow{\sigma _k}\}$, such that $\tau$ are the types for the variables in the head of the clause in $\varGamma$ and $\sigma _i$ are the types for the variables in each recursive call.

Example 7

Consider the following predicate:

the output of applying the generate function to the predicate is:

$generate(list(X) :- X = [~]; X = [Y|Ys], list(Ys)) = \{bool, \{X:\sigma _1, Y:\sigma _2, Ys:\sigma _3\}, \{\alpha = [~], \beta = [\delta ~|~\epsilon ]\}, \{\sigma _3 \le \sigma _1, \sigma _1 \le \sigma _3\}, \{\sigma _1 = \alpha + \beta , \sigma _2 = \delta , \sigma _3 = \epsilon \}\}$.

The set $\{\sigma _3 \le \sigma _1, \sigma _1 \le \sigma _3\}$ comes from the recursive call to the predicate, while $\alpha = [~]$ comes from $X = [~]$, and $\beta = [\delta ~|~\epsilon ]$ comes from $X = [Y|Ys]$. The definition $\sigma _1 = \alpha + \beta$ comes from the application of the $\oplus$ operation.

5.3 Constraint Solving

Let Eq be a set of equality constraints, Ineq be a set of subtyping constraints, and $\varDelta$ a set of type definitions. Function $solve(Eq,Ineq,\varDelta )$ is a rewriting algorithm that solves the constraints, outputting a pair of a substitution and a new set of type definitions. Note that the rewriting rules in the following definitions of the solver algorithm are assumed to be ordered.

Definition 9

A set of equality constraints is in solved form if:

• all constraints are of the form $\alpha _i = \tau _i$;

• there are no two constraints with the same $\alpha _i$ on the left hand side;

• no type variables on the left-hand side of the equations occurs on the right-hand side of equations.

A set of equality constraints in normal form can be interpreted as a substitution, where each constraint $\alpha _i = \tau _i$ corresponds to a substitution for the type variable $\alpha _i$, $[\alpha _i \mapsto \tau _i]$.

A configuration is either the term fail (representing failure), a pair of a substitution and a set of type definitions (representing the end of the algorithm), or a triple of a set of equality constraints Eq, a set of subtyping constraints Ineq, and a set of type definitions $\varDelta$. The following rewriting algorithm consists of the transformation rules on configurations.

$solve(Eq,Ineq,\varDelta ) =$

• 1. $(\{\tau = \tau \} \cup Eq,Ineq,\varDelta ) \rightarrow (Eq,Ineq,\varDelta )$

• 2. $(\{\alpha = \tau \} \cup Eq,Ineq,\varDelta ) \rightarrow (\{\alpha = \tau \} \cup Eq[\alpha \mapsto \tau ],Ineq[\alpha \mapsto \tau ],\varDelta [\alpha \mapsto \tau ])$, if type variable $\alpha$ occurs in Eq, Ineq, or $\varDelta$

• 3. $(\{\tau = \alpha \} \,\cup \, Eq,Ineq,\varDelta ) \rightarrow (\{\alpha = \tau \} \,\cup \, Eq,Ineq,\varDelta )$, where $\alpha$ is a type variable and $\tau$ is not a type variable

• 4. $(\{f(\tau _1,\dots ,\tau _n) = f(\tau \prime _1,\dots ,\tau \prime _n)\} \,\cup \, Eq,Ineq,\varDelta \rightarrow (\{\tau _1 = \tau \prime _1, \dots , \tau _n = \tau \prime _n\} \,\cup \, Eq,Ineq,\varDelta$

• 5. $(\{f(\tau _1,\dots ,\tau _n) = g(\tau \prime _1,\dots ,\tau \prime _m)\}\cup Eq, Ineq,\varDelta ) \rightarrow fail$

• 6. $(Eq,\{\tau \le \tau \} \cup Ineq,\varDelta ) \rightarrow (Eq,Ineq,\varDelta )$

• 7. $(Eq,\{f(\tau _1,\dots ,\tau _n) \le f(\tau \prime _1,\dots ,\tau \prime _n)\} \cup Ineq, \varDelta ) \rightarrow (Eq,\{\tau _1 \le \tau \prime _1, \dots \tau _n \le \tau \prime _n\} \cup Ineq,\varDelta )$

• 8. $(Eq,\{\alpha \le \tau _1, \dots , \alpha \le \tau _n\} \cup Ineq, \varDelta ) \rightarrow (Eq\cup Eq\prime ,\{\alpha \le \tau \} \cup Ineq, \varDelta \prime )$,

  where $\alpha$ is a type variable, $n \ge 2$, and $intersect(\tau _1,\dots ,\tau _n,\varDelta ,I) = (\tau ,Eq\prime ,\varDelta \prime )$

• 9. $(Eq,\{\alpha \le \tau \} \cup Ineq,\varDelta ) \rightarrow (Eq \cup \{\alpha = \tau \},Ineq,\varDelta )$,

  where $\alpha$ is a type variable and no other constraints exist with $\alpha$ on the left-hand side

• 10. $(Eq,\{\tau _1 + \dots + \tau _n \le \tau \} \cup Ineq, \varDelta ) \rightarrow (Eq,\{\tau _1 \le \tau , \dots , \tau _n \le \tau \} \cup Ineq, \varDelta )$

• 11. $(Eq,\{\sigma \le \tau \} \cup Ineq,\varDelta ) \rightarrow (Eq,Ineq,\varDelta )$,

  if $(\sigma$,$\tau$) are on the store of pairs of types that have already been compared

• 12. $(Eq,\{\sigma \le \tau \} \cup Ineq,\varDelta ) \rightarrow (Eq,\{Rhs_{\sigma } \le \tau \} \cup Ineq, \varDelta )$,

  where $\sigma$ is a type symbol, and $\sigma = Rhs_{\sigma } \in \varDelta$. Also add $(\sigma ,\tau )$ to the store of pairs of types that have been compared

• 13. $(Eq,\{\tau _1 \le \alpha , \dots \tau _n \le \alpha \} \cup Ineq,\varDelta ) \rightarrow (Eq \cup \{\alpha = \tau _1 + \dots + \tau _n\},Ineq,\varDelta )$

• 14. $(Eq,\{\tau \le \tau _1 + \dots + \tau _n\}\cup Ineq,\varDelta ) \rightarrow (Eq,\{\tau \le \tau _i\}\cup Ineq,\varDelta )$,

  where $\tau _i$ is one of the summands

• 15. $(Eq,\{\tau \le \sigma \}\cup Ineq,\varDelta ) \rightarrow (Eq,Ineq,\varDelta )$,

  if $(\sigma$,$\tau$) are on the store of pairs of types that have already been compared

• 16. $(Eq,\{\tau \le \sigma \}\cup Ineq,\varDelta ) \rightarrow (Eq,\{\tau \le Rhs_{\sigma }\}\cup Ineq,\varDelta )$,

  where $\sigma$ is a type symbol, and $\sigma = Rhs_{\sigma } \in \varDelta$. Also add $(\sigma ,\tau )$ to the store of pairs of types that have been compared

• 17. $(Eq,\emptyset ,\varDelta ) \rightarrow (Eq,\varDelta \prime )$

• 18. otherwise $\rightarrow$ fail.

Note that an occur check is required in steps 2, 9, and 13. This rewriting algorithm is based on the one described in [Mah88] for equality constraints, and an original one for the subtyping constraints. We will now show an example of the execution of the algorithm on the output of the constraint generation algorithm, showed in Example 7.

Example 8

Following Example 7, applying solve to the tuple $(Eq,Ineq,\varDelta )$, corresponding to $(\{X:\sigma _1, Y:\sigma _2, Ys:\sigma _3\}, \{\alpha = [~], \beta = [\delta ~|~\epsilon ]\}, \{\sigma _3 \le \sigma _1, \sigma _1 \le \sigma _3\}, \{\sigma _1 = \alpha + \beta , \sigma _2 = \delta , \sigma _3 = \epsilon \})$:

$(\{\alpha = [~], \beta = [\delta ~|~\epsilon ]\},\{\sigma _3 \le \sigma _1, \sigma _1 \le \sigma _3\},\{\sigma _1 = \alpha + \beta , \sigma _2 = \delta , \sigma _3 = \epsilon \}) \rightarrow _2$

$(\{\alpha = [~], \beta = [\delta ~|~\epsilon ]\},\{\sigma _3 \le \sigma _1, \sigma _1 \le \sigma _3\},\{\sigma _1 = [~] + \beta , \sigma _2 = \delta , \sigma _3 = \epsilon \}) \rightarrow _2$

$(\{\alpha = [~], \beta = [\delta ~|~\epsilon ]\},\{\sigma _3 \le \sigma _1, \sigma _1 \le \sigma _3\},\{\sigma _1 = [~] + [\delta ~|~\epsilon ], \sigma _2 = \delta , \sigma _3 = \epsilon \}) \rightarrow _{12}$

$(\{\alpha = [~], \beta = [\delta ~|~\epsilon ]\},\{\epsilon \le \sigma _1, \sigma _1 \le \sigma _3\},\{\sigma _1 = [~] + [\delta ~|~\epsilon ], \sigma _2 = \delta , \sigma _3 = \epsilon \}) \rightarrow _{9}$

$(\{\alpha = [~], \beta = [\delta ~|~\epsilon ],\epsilon = \sigma _1\},\{\sigma _1 \le \sigma _3\},\{\sigma _1 = [~] + [\delta ~|~\epsilon ], \sigma _2 = \delta , \sigma _3 = \epsilon \}) \rightarrow _{2}$

$(\{\alpha = [~], \beta = [\delta ~|~\sigma _1],\epsilon = \sigma _1\},\{\sigma _1 \le \sigma _3\},\{\sigma _1 = [~] + [\delta ~|~\sigma _1], \sigma _2 = \delta , \sigma _3 = \sigma _1 \}) \rightarrow _{s}$

$(\{\alpha = [~], \beta = [\delta ~|~\sigma _1],\epsilon = \sigma _1\},\{\sigma _1 \le \sigma _1\},\{\sigma _1 = [~] + [\delta ~|~\sigma _1], \sigma _2 = \delta \}) \rightarrow _{6}$

$(\{\alpha = [~], \beta = [\delta ~|~\sigma _1],\epsilon = \sigma _1\},\emptyset ,\{\sigma _1 = [~] + [\delta ~|~\sigma _1], \sigma _2 = \delta \})$

Note that the resulting set of constraints only contains constraints in solved form, that can be seen as a substitution. Step $\rightarrow _{s}$, stands for the following simplification step: if two type definitions are equal, we delete one of them and replace every occurrence of the type symbol by the other. Therefore, the resulting context $\varGamma$ is $\{X:\sigma _1, Y:\sigma _2, Ys:\sigma _1\}$.

Type intersection is calculated as follows, $intersect(\tau _1,\tau _2,\varDelta ,I) = (\tau ,Eq\prime ,\varDelta \prime )$, where:

• if both $\tau _1$ and $\tau _2$ are type variables, then $\tau = \tau _2, \varDelta \prime = \varDelta , Eq\prime = \{\tau _1 = \tau _2\}$.

• if $\tau _1 = \tau _2$, then $\tau = \tau _1, \varDelta \prime = \varDelta , Eq\prime = \emptyset$.

• if $(\tau _1,\tau _2,\tau _3) \in I$, then $\tau = \tau _3, \varDelta \prime = \varDelta , Eq\prime = \emptyset$.

• if $\tau _1$ is a type variable, then $\tau = \tau _2, \varDelta \prime = \varDelta , Eq\prime = \emptyset$.

• if $\tau _2$ is a type variable, then $\tau = \tau _1, \varDelta \prime = \varDelta , Eq\prime = \emptyset$.

• if $\tau _1 = \sigma _1, \tau _2 = \sigma _2$, and $(\bar{\tau },Eq,\varDelta _2) = cpi(\bar{\tau _1},\bar{\tau _2},\varDelta ,I \cup \{(\tau _1,\tau _2,\tau _3)\})$, then $\tau = \tau _3, \varDelta \prime = \varDelta _2 \cup \{\tau _3 = \bar{\tau }\},Eq\prime = Eq$, where $\sigma _1 = \bar{\tau _1}, \sigma _2 = \bar{\tau _2} \in \varDelta$ and $\tau _3$ is fresh.

• if $\tau _1 = \sigma _1, \tau _2 = f(t_1,\dots ,t_n)$, and $(\bar{\tau },Eq,\varDelta _2) = cpi(\bar{\tau },\tau _2,\varDelta ,I \cup \{(\tau _1,\tau _2,\tau _3)\})$, then $\tau = \tau _3, \varDelta \prime = \varDelta \cup \{\tau _3 = \bar{\tau }\},Eq\prime = Eq$, where $\sigma _1 = \bar{\tau _1} \in \varDelta$ and $\tau _3$ is fresh. Same for $\tau _2 = \sigma _1$ and $\tau _1 = f(t_1,\dots ,t_n)$.

• if $\tau _1 = f(\tau _1,\dots ,\tau _n), \tau _2 = f(\tau \prime _1,\dots ,\tau \prime _n)$, then $\forall i. 1 \le i \le n$, $(\tau \prime \prime _i,Eq_i,\varDelta _i) = intersect(\tau _i, \tau \prime _i,\varDelta ,I)$, $\tau = f(\tau \prime \prime _1,\dots ,\tau \prime \prime _n), \varDelta \prime = \varDelta _1 \cup \dots \cup \varDelta _n, Eq\prime = Eq_1 \cup \dots \cup Eq_n$.

• otherwise fail.

$cpi(\bar{\tau _1},\bar{\tau _2},\varDelta ,I)$ is a function that applies $intersect(\tau ,\tau \prime ,\varDelta ,I)$ to every pair of types $\tau ,\tau \prime$, such that $\tau \in \bar{\tau _1}$ and $\tau \prime \in \bar{\tau _2}$, and gathers all results as the output.

This intersection algorithm is based on the one presented in [Zob87], with a few minor changes. The difference is that our types can be type variables, which could not happen in Zobel’s algorithm, since intersection was only calculated between ground types. To deal with this extension, in our algorithm type variables are treated as Zobel’s any type, except when both types are type variables, in which case we also unify them. Termination and correctness of type intersection for a tuple distributive version of Zobel’s algorithm was proved previously in [Lu01] and replacing the any type with type variables maintains the same properties, because our use of type intersection considers types where type variables occur only once, thus they can be safely replaced by Zobel’s any type. Note that we deal with type variables which occur more than once but with calls to type unification.

5.4 Decidability

The next theorem shows that both the equality constraint and subtyping constraint solvers terminate at every input set of constraints.

Theorem 1 (Termination)

solve always terminates, and when solve terminates, it either fails or the output is a pair of a substitution and a new set of type definitions.

The proof for this theorem follows a usual termination proof approach, where we show that a carefully chosen metric decreases at every step.

To guarantee that the output set of equality constraints is in normal form, in order to be interpreted as a substitution, we also prove the lemma below.

Lemma 1

If $solve(Eq,Ineq,\varDelta ) \rightarrow ^{*} (S,\varDelta \prime )$, then S is in normal form.

5.5 Soundness

Here we prove that the type inference algorithm is sound, in the sense that inferred types are derivable in the type system, which defines well-typed programs. For this we need the following auxiliary definitions and lemmas which are used in the proofs of the main theorems.

The following lemmas state properties of the constraint satisfaction relation $\models$, subtyping, and the type intersection operation.

Lemma 2

If we have S such that $S \,\models \, C \cup C\prime$, then $S \,\models \, C$ and $S\,\models \, C\prime$.

Lemma 3

If $S \,\models \, Eq$ such that $(\varGamma ,\varDelta ,Eq) = \otimes ((\varGamma _1, \dots , \varGamma _n),(\varDelta _1, \dots , \varDelta _n))$, and $\forall i.\varGamma _i,S(\varDelta _i) \vdash M_i: S(\tau _i)$ then $\forall i.\varGamma , S(\varDelta ) \vdash M_i : S(\tau _i)$.

Lemma 4

If we know for all $i = 1,\dots , n$ that $\varGamma _i, S(\varDelta _i) \vdash b_i : bool$ and we know $(\varGamma ,\varDelta ) = \otimes ((\varGamma _1,\dots ,\varGamma _n),(\varDelta _1,\dots ,\varDelta _n))$, then $\varGamma ,S(\varDelta ) \vdash b_i:bool$.

Lemma 5

Let $\tau _1,\dots ,\tau _n,\tau$ be types such that $\forall i. \tau _i \sqsubseteq \tau$. Then $\tau _1 + \dots + \tau _n \sqsubseteq \tau$.

Lemma 6

Let $\tau _1,\dots ,\tau _n,\tau$ be types such that $\exists i. \tau \sqsubseteq \tau _i$. Then $\tau \sqsubseteq \tau _1 + \dots + \tau _n$.

Lemma 7

If $intersect(\tau _1,\tau _2,I,\varDelta ) = (\tau ,Eq,\varDelta \prime )$, then $\tau \sqsubseteq \tau _1$, and $\tau \sqsubseteq \tau _2$.

Proposition 1

If Eq is a set of equality constraints in normal form, then $Eq \,\models \, Eq$.

Now we have a theorem for the soundness of constraint generation which states that if one applies a substitution which satisfies the generated constraints to the type obtained by the constraint generation function, we get a well-typed program.

Theorem 2 (Soundness of Constraint Generation)

For a program, query, or term P, if $generate(P) = (\tau ,\varGamma ,Eq,Ineq,\varDelta )$, then for any $S \,\models \, Eq,Ineq$, we have $\varGamma ,S(\varDelta )\vdash P:S(\tau )$.

We also proved the soundness of constraint solving, which basically shows that the solved form returned by our constraint solver for a set of constrains C satisfies C.

Theorem 3 (Soundness of Constraint Solving)

Let Eq be a set of equality constraints, Ineq a set of subtyping constraints, and $\varDelta$ a set of type definitions. If $solve(Eq,Ineq,\varDelta ) \rightarrow ^{*} (S,\varDelta \prime )$ then $S \,\models \, Eq,Ineq$.

Finally, using the last two theorems we prove the soundness of the type inference algorithm. The soundness theorem states that if one applies the substitution corresponding to the solved form returned by the solver to the type obtained by the constraint generation function, we get a well-typed program.

Theorem 4 (Soundness of Type Inference)

Given P, if $generate(P) = (\tau ,\varGamma ,Eq,Ineq,\varDelta )$ and $solve(Eq,Ineq,\varDelta ) \rightarrow ^{*} (S,\varDelta \prime )$, then $\varGamma ,S(\varDelta \prime ) \vdash P:S(\tau )$.

6 Related Work

Types have been used before in Prolog systems: relevant works on type systems and type inference in logic programming include types used in the logic programming systems CIAO Prolog [SG95, VB02], SWI and Yap [SCWD08]. CIAO uses types as approximations of the success set, while we use types as filters to the program semantics. There is an option where the programmer gives the types for the programs in the form of assertions, which is recommended in [PCPH08]. The well-typings given in [SBG08], also have the property that they never fail, in the sense that every program has a typing, which is not the case in our algorithm, which will fail for some predicates. The previous system of Yap only type checked predicate clauses with respect to programmer-supplied type signatures. Here we define a new type inference algorithm for pure Prolog, which is able to infer data types.

In several other previous works types approximated the success set of a predicate [Zob87, DZ92, YFS92, BJ88]. This sometimes led to overly broad types, because the way logic programs are written can be very general and accept more than what was initially intended. These approaches were different from ours in the sense that in our work types can filter the success set of a predicate, whenever the programmer chooses to do so, using the closure operation, or data type declarations.

A different approach relied on ideas coming from functional programming languages [MO84, LR91, HL94, SCWD08]. Other examples of the influence of functional languages on types for logic programming are the type systems used in several functional logic programming languages [Han13, SHC96]. Along this line of research, a rather influential type system for logic programs was Mycroft and O’Keefe type system [MO84], which was later reconstructed by Lakshman and Reddy [LR91]. This system had types declared for the constants, function symbols and predicate symbols used in a program. Key differences from our work are: 1) in previous works each clause of a predicate must have the same type. We lift this limitation extending the type language with sums of types, where the type of a predicate is the sum of the types of its clauses; 2) although we may use type declarations, they are optional and we can use a closure operation to infer datatype declarations from untyped programs.

Set constraints have also been used by many authors to infer types for logic programming languages [HJ92, GdW94, TTD97, CP98, DMP00, DMP02]. Although these approaches differ from ours since they follow the line of conservative approximations to the success set, we were inspired from general techniques from this area to define our type constraint solvers.

7 Final Remarks

In this paper, we present a sound type inference algorithm for pure Prolog. Inferred types are semantic approximations by default, but the user may tune the algorithm, quite easily, to automatically infer types which correspond to the usual data types used in the program. Moreover, the algorithm may also be tuned to use predefined (optional) data type declarations to improve the output types. We proved the soundness of the algorithm, but completeness (meaning that the inferred types are a finite representation of all types which make the program well-typed) is an open problem for now. We strongly suspect that the algorithm is complete without closure, but could not prove it yet. On the implementation side we are now extending $YAP^T$ to deal with full Prolog to be able to apply it to more elaborated programs. This includes built-ins and mutually recursive predicates. For this, we will have predefined rules for every built-in predicate and we are also extending the algorithm to generate constraints not for single predicates, but for each strongly connected component on the dependency graph of the program.