janvier  2006  –  Journées  Francophones  des  Langages  Applicatifs–  JFLA06

Decidable type inference for the polymorphic rewriting calculus

Horatiu Cirstea^{1} & Claude Kirchner^{2} & Luigi Liquori^{3} & Benjamin Wack^{4}

1: University of Nancy II & LORIA^{∗}  Horatiu.Cirstea@loria.fr

                       2: INRIA & LORIA^{∗}  Claude.Kirchner@loria.fr
                       3: INRIA Sophia Antipolis  Luigi.Liquori@inria.fr

4: University Henri Poincaré & LORIA^{∗} Benjamin.Wack@loria.fr

Résumé

The rewriting calculus (ρ-calculus), is a minimal framework embedding λ-calculus and Term Rewriting Systems, that allows abstraction on variables and patterns. The ρ-calculus features higher-order functions (from λ-calculus) and pattern matching (from Term Rewriting Systems). In this paper, we study extensively the decidability of type inference in the second-order ρ-calculus à la Curry (rhoStk).

1. Introduction

A promising line of research unifying the logic paradigm with the functional paradigm is that of rewrite-based languages [MOM02] like, for example, ELAN [The04d], Maude [The04c], ASF+SDF [The04a], Obj^{∗} [FN96, Gog04]). This kind of languages have been successfully used for theorem proving [BCM04], constraint solving [Cas96], model-checking [EMS03, CMR04], program transformation [vdBKV96], etc. Moreover, rewrite-based programming can be integrated in other languages [MRV03] as “formal islands” (that we can reason on) in the middle of imperative programs [MRV03, KMR05].

The main mechanism the rewrite-based languages are based on is the pattern-matching which allows one to discriminate between alternatives. Each pattern is associated with an action ; once an instance of a pattern is recognized, the corresponding term is rewritten to a new one.

Useful applications of pattern-matching lie in the field of pattern recognition, and strings/trees manipulation. It has also been widely used in functional and logic programming, for instance in ML [MTHM97, The03a], Haskell [The04b], Scheme [The04e], or Prolog [The03b]. However, in all these applications, pattern-matching is considered as a convenient mechanism for expressing complex requirements about the function’s argument, rather than a basis for a paradigm of computation. We argue that the computational behavior of a calculus can be deeply influenced by the presence of pattern-matching and we support this statement by studying the (typing related) properties of a calculus that strongly relies on the matching mechanism.

One of the most commonly used models of computation, the lambda calculus, uses only trivial pattern-matching. This calculus has recently been extended, initially for programming concerns, either by introducing patterns in Lambda-calculi [Pey87, vO90], or by introducing matching and rewrite rules in functional languages. More concerned with extending logics, Stehr has studied a Calculus of Constructions enhanced with rewriting logic [Ste02].

Cirstea & Kirchner & Liquori & Wack

The rewriting calculus [CKL01b, CLW04] is a foundational framework integrating matching, rewriting and functions in a uniform way. Its abstraction mechanism is based on the rewrite rule formation : in a term of the form P ⇾ A, one abstracts over the (free variables of the) pattern P.

0LORIA: UMR 7506, CNRS, INRIA, INPL, UHP, Université de Nancy II.

If an abstraction P ⇾ A is applied to the term B, then the evaluation mechanism is based on the instantiation (in A) of the free variables present in P with the appropriate subterms of B. Indeed, this instantiation is achieved by matching P against B.

As a foundational calculus, the rewriting calculus is a non-trivial generalization of the lambda calculus, since we get the lambda calculus back if every pattern P is a variable. Term rewrite systems can also be conveniently modeled in the rewriting calculus [CLW04] by using the structure operator for representing the corresponding sets of rewrite rules as ρ-terms. In particular, the notions of rule application and result (basic ingredients of term rewrite systems) become explicit in the rewriting calculus.

In the rewriting calculus, a rewrite rule is a first-class citizen, which can be created, manipulated and modified during the evaluation. The abilities to manipulate rules and to define strategies guiding their application represent the basic methods in rewrite-based languages and thus the rewriting calculus can be used as a core engine calculus for this kind of languages.

It is well known that static analysis via a type system enforces a safer programming discipline. We present and analyze here a powerful polymorphic type system for the rewriting calculus that can be seen as a good candidate for giving the static semantics of a family of rewrite-based languages such as ELAN and Maude.

In [LW05] we have introduced a ρ-calculus à la Church (called RhoF) featuring second-order polymorphic types. In this fully typed second-order rewriting calculus, the types of the bound variables are specified in the term, making type reconstruction and verification quite straightforward. Moreover, this calculus enjoys classical type related properties such as subject reduction, and type uniqueness.

We have also proposed a classical erasing function [Cur34, Lei83, GR88] that can be applied to RhoF in order to obtain a corresponding type inference system à la Curry. In Rho|F|, the calculus à la Curry, type information is not given in the term, and the type system is not fully syntax-directed, thus enforcing a flexible polymorphic type discipline. When we look at the ρ-calculus as a kernel calculus underneath a pattern-matching based programming language, this approach corresponds to ELAN, or Maude, or Obj^{∗}, or ASF+SDF, or Haskell, or ML-like languages, where the user can write programs in a completely untyped language, and types are automatically inferred at compilation-time. Type inference can be also intended as the construction of an abstract interpretation of the program, that can be used as a correctness criterion. Unfortunately, as it is well-known for the λ-calculus [Wel99], the type assignment problem for Rho|F| is undecidable.

We introduce in what follows a restriction of Rho|F|, called rhoStk, where the polymorphic types are clearly separated from the polymorphic type schemes. We discuss its expressive power and we present a type inference algorithm. We compare our approach to similar ones used in functional programming languages and more precisely in ML.

Synopsis In the next section we introduce the syntax and semantics of rhoStk together with a relation defining in some sense the definitive matching failures that one wants normally to eliminate from the final result of an evaluation. We introduce then the typing system and the type inference algorithm that is proved sound, correct and principal. In Section 3 we briefly compare the approach presented here with the one used in ML. The final section concludes and gives some possible directions for future research. The complete proofs of the properties stated in the paper are available in [Wac05, CKLW06].

Damas-Milner type inference algorithm for the Rewriting Calculus

K ∈ K
τ.ι ∈ Type
σ ∈ TypeScheme
Γ.Δ ∈ Context
P.Q ∈ P
A.B.f ∈ T

K ::= ∗
τ ::= α | ι\overline{α} | τ ⇾ τ
σ ::= ∀\overline{α}.τ
Δ ::= ∅ | Δ, f:σ | Δ, X:σ
P ::= stk | X | f(\overline{P}) (all vars occur only once in any P)
A ::= stk | f | X | P ⇾ A | let P ≪ A in A | A A | A ≀ A

Fig. 1 – Syntax of rhoStk

2. Type inference in rhoStk

We now define rhoStk, a polymorphic rewriting calculus à la Curry where type information is not given in the term. In order to recover the decidability of the type inference, polymorphic types are clearly separated from the polymorphic type schemes. We discuss the expressive power of the introduced calculus and we present a type inference algorithm.

2.1. Syntax

We consider the meta-symbols “_⇾ _” (function- and type-abstraction), and “let _≪ _in _” (delayed matching constraint), and “_≀ _” (structure operator). The application operator is denoted by concatenation. We assume that the application operator associates to the left, while the other operators associate to the right. The priority of the application is higher than that of “let _≪ _in _” which is higher than that of “_⇾ _“ which is, in turn, of higher priority than the “_≀ _”. The symbol τ ranges over the set Type of types, the symbol ι ranges over the set Type_{K} of type constants, the symbols α, β range over the set Type_{V} of type-variables, the symbol σ ranges over the set TypeScheme of type schemes, the symbols A, B, C, …, U, V, W range over the set T of (un)typed terms, the symbols X, Y, Z, … range over the set V of term variables, the symbols a, b, c, …, f, g, h, … range over a set Term_{K} of term constants. The symbols P, Q range over the set P of patterns and the symbols θ, ϕ, ψ range over substitutions. We denote \overline{A} for A_{1} ⋯ A_{n}, for n ≥ 0. The application of a constant, say f, to a term A will be usually denoted by f(A), following the algebraic folklore ; this convention can be curryfied in order to denote a function taking multiple arguments, e.g. f(\overline{A}) ≜ f(A_{1}, ⋯, A_{n}) ≜ (⋯ (f A_{1}) ⋯ A_{n}).

The syntax of rhoStk is presented in Figure 1. As one would expect, the types allow us to define a polymorphic type system (i.e. type-variables can be bound in types through the “∀” binder). The patterns are algebraic terms (i.e. terms constructed only with variables, constants and applications) which can be used as left-hand sides of the rewrite rules ; the set of patterns is obviously included in the set of terms. The well-known linearity restriction [vO90] is needed to keep the small-step semantics confluent. A rewrite rule of the form P ⇾ A abstracting over the variables of P is a first-class citizen of the calculus. An application is implicitly denoted by concatenation. The delayed matching constraint let P ≪ A in B can be seen as the term B with its free-variables constrained by the matching between P and A. The symbol stk is the special constant representing all the definitive (matching) failures.A structure is a collection of terms that can be seen either as a set of rewrite rules or as a set of results. The variables of the left-hand side of a rewrite rule are bound in a usual way.

Definition 2.1 (Free-variables FV)

\begin{matrix}FV(f) & ≜ & ∅ \\ FV(stk) & ≜ & ∅ \\ FV(X) & ≜ & \{X\} \\ FV(α) & ≜ & \{α\} \end{matrix}  \begin{matrix}FV(P ⇾ A) & ≜ & FV(A) \ FV(P) \\ FV(let P ≪ A in B) & ≜ & FV((P ⇾ B) A) \\ FV(A B) & ≜ & FV(A) ∪ FV(B) \\ FV(A ≀ B) & ≜ & FV(A) ∪ FV(B) \\ FV(τ_{1} ⇾ τ_{2}) & ≜ & FV(τ_{1}) ∪ FV(τ_{2}) \end{matrix}

As usual, we work modulo α-conversion and we adopt Barendregt’s “hygiene-convention” [Bar84], i.e. free- and bound-variables have different names. Since these assumptions avoid the variable capture problems, the definition of substitution applications is straightforward.

Definition 2.2 (Substitutions) A substitution θ is a mapping from the set of term variables (resp. type variables) to the set of terms (resp. types). A finite substitution θ has the form {A_{1}/X_{1} … A_{m}/X_{m}}, or {τ_{1}/α_{1} … τ_{m}/α_{m}}, and its domain Dom(θ) denotes {X_{1}, …, X_{m}}, resp. {α_{1}, …, α_{m}}. The application of a substitution θ to a term A (resp. type τ, resp. context Δ), denoted by Aθ (resp. τθ, resp. Δθ), is defined as follows :

X_{i}θ  ≜ \{ \begin{matrix}A_{i} & ifX_{i} ∈ Dom(θ) \\ X_{i} & otherwise \end{matrix}
fθ  ≜ f
stkθ  ≜ stk
(P ⇾ A)θ  ≜ P ⇾ Aθ
(A B)θ  ≜ Aθ Bθ
(A ≀ B)θ  ≜ Aθ ≀ Bθ
(let P ≪ A in B)θ ≜ (let P ≪ Aθ in Bθ)

α_{i}θ  ≜ \{ \begin{matrix}τ_{i} & if α_{i} ∈ Dom(θ) \\ α_{i} & otherwise \end{matrix}
ιθ  ≜ ι
∅θ  ≜ ∅
(τ_{1} ⇾ τ_{2})θ ≜ τ_{1}θ ⇾ τ_{2}θ
(Δ, X:τ)θ ≜ Δθ, X:τθ
(Δ, f:τ)θ ≜ Δθ, f:τθ

2.2. Semantics

The evaluation mechanism of the calculus relies on the fundamental operation of matching that allows us to bind variables to their current values. Since we want to define an expressive and powerful calculus, we allow the matching to be performed modulo a congruence on terms. This congruence used at matching time is a fundamental parameter of the calculus and different instances are obtained when instantiating this parameter by a congruence defined, for example, syntactically, or equationally or in a more elaborated way [CKL01a].

For the purpose of this paper we restrict to syntactic matching and we say that a substitution θ is solution of the matching-equation A ≺≺ B if Aθ ≡ B, i.e.Aθ and B and identical. The unique solution of such a matching problem is denoted θ_{A≺≺B}.

It is sometimes interesting to handle uniformly the (definitive) matching failures and to eliminate them when not significant for the computation. We want thus to represent by stk all the delayed matching constraints whose corresponding matching problem is unsolvable independently of subsequent instantiations and reductions, and thus we intuitively want to define stk by the rule :

∄θ, P θ =_{ρσδ} Nθ
let P ≪ N in M →_{stk} stk

where =_{ρσδ} is the congruence induced by the first three evaluation rules given in Figure 2. The conditions of this reduction rule are undecidable but we can define a sufficient condition guaranteeing that a given term will never match a given pattern.

Damas-Milner type inference algorithm for the Rewriting Calculus

(P ⇾ A) B →_{ρ} let P ≪ B in A
let P ≪ B in A →_{σ} Aθ_{(P≺≺B)}  Provided θ exists
(A ≀ B) C →_{δ} A C ≀ B C
A →_{stk} B  As defined in Definition 2.4

Fig. 2 – Top-level Rules of rhoStk

Definition 2.3 (Superposition) The relation ⋢ is defined on P × T as follows :

stk ⋢ g(N_{1}, …, N_{n})  f(P_{1}, …, P_{m}) ⋢ stk
stk ⋢ P ⇾ N  f(P_{1}, …, P_{m}) ⋢ P ⇾ N
f(P_{1}, …, P_{m}) ⋢ g(N_{1}, …, N_{n})  if f ≢ g or n ≠ m or ∃i, P_{i} ⋢ N_{i}
f(P_{1}, …, P_{m}) ⋢ let P ≪ N in M  if P ⋢ N or f(P_{1}, …, P_{m}) ⋢ M

Lemma 2.1 (Correction of ⋢) For any P and M, if P ⋢ M then

∀θ_{1}, θ_{2}, ∀M′, Mθ_{1} ↦ →_{ρσδ}^{stk} M′ ⇒ P θ_{2} ≢ M′

Corollary 2.1 (Stability of ⋢) The relation P ⋢ M is stable by substitution and reduction of M.

Starting from the superposition relation, we define a reduction relation that eliminates definitively stuck subterms.

Definition 2.4 The relation →_{stk} is defined by the following rules :

let P ≪ A in B →_{stk} stk  if P ⋢ A
stk ≀ A  →_{stk} A
A ≀ stk  →_{stk} A
stk A  →_{stk} stk

We denote by ↦_{stk} the contextual closure induced by these rules. Its reflexive and transitive closure is denoted by ↦ →_{stk}.

Figure 2 shows the reduction rules of rhoStk : (ρ) this rule triggers the application of an abstraction to a term, but does not immediately try to

solve the associated matching equation. (σ) this rule applies if and only if the matching equation P ≺≺ B has a solution : in this case the

matching solution is computed and applied to the term A. If there is no solution, this rule does not apply. As we shall see, further reductions or instantiations are likely to modify B so that the equation has a solution and the rule can be triggered.

(δ) this rule distributes structures on the left-hand side of the application. This gives the possibility,

for example, to apply in parallel two distinct pattern-abstractions A and B to a term C. (stk) pushes into the operational semantics the rewrite rules dealing with the elimination of the

definitive failures. We denote by ↦_{ρσδ} the contextual closure induced by the rules (ρ), (δ) and (σ). Its reflexive and transitive closure is denoted by ↦ →_{ρσδ}. The symmetric and transitive closure of ↦ →_{ρσδ} is denoted by =_{ρσδ}. We denote by ↦_{ρσδ}^{stk} the relation ↦_{stk} ∪ ↦_{ρσδ} and by ↦ →_{ρσδ}^{stk} its reflexive and transitive closure.

Theorem 2.1 (Confluence of rhoStk [CLW04, Wac05]) The relation ↦_{ρσδ}^{stk} is confluent.

Example 2.1 (Computing the length of a list) Let use define the ρ-term

len ≜ rec S ⇾ ( \begin{matrix}nil & ⇾ 0 \\ ≀ \\ (cons X L) & ⇾ suc (S (rec S) L) \end{matrix} )

where rec, nil, 0, cons, suc are constants. Then the ρ-term len (rec len) computes the length of any list that is given as an argument. We should mention that if the evaluation is performed using only ↦ →_{ρσδ} then the final result is a structure containing the expected result and several delayed matching constraints in normal form. When ↦ →_{ρσδ}^{stk} is used, the final result consists only off the expected term.

It is interesting to see that, if we erase all the occurrences of S and rec, we get the classical rewrite system computing the length of lists.

2.3. Typing Rules

As we have already mentioned, the type assignment system for Rho|F| is undecidable. One of the problems that is peculiar to this calculus is the ability to define any number of constants with a given type, without really considering them as constructors. Thus, in Rho|F|, a constant can have a type f : ∀α. (α → ι) where the parameter α does not appear explicitly in the rightmost type ι. Then when typing

let f(X) ≪ f(Y ⇾ Y) in (X 1)

the pattern f(X) gets type ι, where the type of Y ⇾ Y is forgotten. Then it is impossible to infer correctly the type of X : a standard algorithm would suggest the most general type ∀β. (int → β), so the type computed for the expression above can be anything.

This typing discipline for constants is unsound : the previous term has type β (for any β) but it reduces to 1, which has type int. Moreover, it leads to undecidability of typing. The inference algorithm could be easily patched to deal with the example above, but the problem is that the pattern could be replaced by a variable Z and the matching against f(X) can then be arbitrarily nested in the body of the delayed matching constraint. Thus, we need to enrich the rightmost term of the type of f with all the type variables appearing in the whole type.

Moreover, a vast amount of types is available in Rho|F| since quantification can occur anywhere in a type. Therefore, we need to restrict polymorphism to well known “type schemes” of the form ∀\overline{α}.τ, where τ is a first-order type, i.e. a monomorphic-type. As example, ∀α.α ⇾ α ≃ {τ ⇾ τ | τ ∈ Type} is the type-scheme for polymorphic identity. Type schemes are equivalent modulo α-conversion. We define simultaneous instantiations of type schemes, via a relation (denoted by ≤) as follows :

τ_{1} ≤ τ_{2} iff τ_{2} ≜ ∀\overline{α}.τ_{3} and τ_{1} ≜ τ_{3}\{\overline{τ}/\overline{α}\} for suitable \overline{τ}.

The resulting type system is given in Figure 3 and proves judgment of the shape :

Γ ⊢ ok and Γ ⊢ τ : ∗ and Γ ⊢ U : τ

We briefly comment some important points concerning the typing rules :

– Formation of admissible type schemes follow some strict rules : every bound variable has to appear in the rightmost type, hence the side condition α ∈ Lab(σ) ;

Damas-Milner type inference algorithm for the Rewriting Calculus

– (T erm·V ar), and (T erm·Const) : the type of a variable/constant is a type instance of its typescheme ; Well-formed Contexts

∅ ⊢ ok (Ctx·Empty)  \begin{matrix}Γ ⊢ ok & X ∉ Dom(Γ) \\ Γ, X:σ ⊢ ok \end{matrix} (Ctx·V ar)

\begin{matrix}Γ ⊢ ok & ι ∉ Dom(Γ) \\ Γ, ι:∗ ⊢ ok \end{matrix} (Ctx·T ypeConst)  \begin{aligned}Γ ⊢ ok & Γ ⊢ σ : ∗ & f ∉ Dom(Γ) \\ & Γ, f:σ ⊢ ok \end{aligned} (Ctx·Const)

\begin{matrix}Γ ⊢ ok & α ∉ Dom(Γ) \\ Γ, α:∗ ⊢ ok \end{matrix} (Ctx·V ar^{∀})

Well-kinded Type (Schemes)

\begin{matrix}α ∈ Lab(σ) & Γ, α:∗ ⊢ σ : ∗ \\ Γ ⊢ ∀α.σ : ∗ \end{matrix} (T ypeScheme^{∀}) {Γ ⊢ ok \atop Γ ⊢ τ : ∗} (T ype)
Lab(ι\overline{α}) = \overline{α}  Lab(τ_{1} ⇾ τ_{2}) = Lab(τ_{2})
Lab(α) = {α}  Lab(∀α.σ) = Lab(σ)

Well-formed Terms and Patterns

\begin{matrix}Γ_{1}, X:σ, Γ_{2} ⊢ ok & σ ≤ τ \\ Γ_{1}, X:σ, Γ_{2} ⊢ X : τ \end{matrix} (T erm·V ar) \begin{matrix}Γ_{1}, f:σ, Γ_{2} ⊢ ok & σ ≤ τ \\ Γ_{1}, f:σ, Γ_{2} ⊢ f : τ \end{matrix} (T erm·Const)

\begin{matrix}Γ, Δ ⊢ P : τ_{1} & BV(CoDomΔ) = ∅ \\ Γ, Δ ⊢ U : τ_{2} & Dom(Δ) = FV(P) \end{matrix} ; Γ ⊢ P ⇾ U : τ_{1} ⇾ τ_{2} (T erm·Abst^{⇾})  \begin{matrix}Γ ⊢ U : τ_{1} ⇾ τ_{2} \\ Γ ⊢ V : τ_{1} \end{matrix} ; Γ ⊢ U V : τ_{2} (T erm·Appl^{⇾})

Γ ⊢ V : τ_{1} Γ, Δ ⊢ P : τ_{1} BV(CoDomΔ) = ∅ Γ, Gen(Δ; Γ) ⊢ U : τ_{2} Dom(Δ) = FV(P) Γ ⊢ let P ≪ V in U : τ_{2} (T erm·Match) \begin{matrix}Γ ⊢ U : τ \\ Γ ⊢ V : τ \end{matrix} ; Γ ⊢ U ≀ V : τ (T erm·Struct)
Gen(τ; Γ) ≜ ∀\overline{α}.τ where \overline{α} = FV(τ) \ FV(Γ) and Gen is extended to contexts.

Fig. 3 – Terms of rhoStk

– (T erm·Abst^{⇾}) : the context Δ has to be inferred, but it can assign only types (not type-schemes) to the variables of P. It corresponds to the behavior of the typing rule for functional abstraction fun x → a in ML.

– (T erm·Match) : this rule performs a restricted form of polymorphic type inference. Again the context Δ used to type P assigns only types to the free variables of P, but when typing U the corresponding type-schemes can be used. It is an enhanced version of the ML let featuring matching.

Lemma 2.2 (Subject Reduction for rhoStk) If Γ ⊢ U : τ and U ↦_{ρδ}^{stk} V, then Γ ⊢ V : τ.

Example 2.2 presents a simple type derivation in rhoStk for the problematic term shown at the beginning of this section.

Example 2.2 (A Simple Type Derivation in rhoStk)

\begin{matrix}(∗) & {β ≤ β \atop Γ, Y:β ⊢ Y : β} ; Γ ⊢ Y ⇾ Y : β ⇾ β \\ Γ ⊢ f(Y ⇾ Y) : κ_{β⇾β} \end{matrix} \begin{matrix}(∗) & {β ⇾ β ≤ β ⇾ β \atop Γ, X : β ⇾ β ⊢ X : β ⇾ β} \\ Γ, X : β ⇾ β ⊢ f(X) : κ_{β⇾β} \end{matrix}\begin{matrix}{ι ⇾ ι ≤ ∀β.(β ⇾ β) \atop Γ, Δ ⊢ X : ι ⇾ ι} & {ι ≤ ι \atop Γ, Δ ⊢ 1 : ι} \\ Γ, Δ ⊢ X 1 : ι \end{matrix}
Γ ⊢ let f(X) ≪ f(Y ⇾ Y) in (X 1) : ι

where Γ ≜ 1:ι, f:∀α.(α ⇾ κ_{α}), and Δ ≜ X:∀β.(β ⇾ β) and (∗) is {(β ⇾ β) ⇾ κ_{β⇾β} ≤ ∀α.(α ⇾ κ_{α}) \atop Γ ⊢ f : (β ⇾ β) ⇾ κ_{β⇾β}}

We see that the pattern f(X) is assigned a type κ_{β⇾β}, ensuring that X has type β ⇾ β. Then generalization gives it type ∀β.(β ⇾ β) when typing the body, which ensures that any type of x is an instance of β ⇾ β.

The next section presents a type inference algorithm (called W^{≪}) that gives a solution to this problem.

Example 2.3 (Typing the term len(rec len))

Let us consider again the term from Example 2.1. If we consider the context

Γ = \{ \begin{matrix}0 : int, suc : int ⇾ int, cons : ∀α.(α ⇾ list_{α} ⇾ list_{α}), nil : ∀α.list_{α}, \\ rec : ∀α.((ι_{α} ⇾ list_{α} ⇾ int) ⇾ ι_{α}) \end{matrix} \}

then, one can check that for any τ we have Γ ⊢ len : ι_{τ} ⇾ list_{τ} ⇾ int and Γ ⊢ len(rec len) : list_{τ} ⇾ int. Indeed, the term len(rec len) takes a list whose elements are of any type, and returns an integer.

The algorithm W^{≪}will compute the principal type list_{β} ⇾ int for len(rec len).

2.4. The Algorithm W^{≪}

We customize the algorithm W of Damas-Milner [DM82] (see also the Caml notes of Pottier [Pot]) and we present an algorithm W^{≪}that takes as input an rhoStk-term U, an environment Γ, and a set of “fresh” type variables V, and (1) checks if it can be well-typed, and (2) infers a principal typing τ for U in Γ, such that :

1. The judgment Γ ⊢ U : τ is derivable

2. If Γ ⊢ U : τ′, then there exists a substitution θ, such that τ′ = τθ.

Definition 2.5 (The Algorithm W^{≪}) The algorithm W^{≪}is given in Figure 4 and uses the classical unification algorithm between first-order terms [JK91] (denoted mgu and omitted here).

Definition 2.6 (Equality out of V) Two substitutions θ_{1} and θ_{2} are equal out of V, written θ_{1} =^{V}∢̸ θ_{2}, if αθ_{1} = αθ_{2}, for all α ∉ V.

Theorem 2.2 (Soundness of W^{≪}) If W^{≪}(Γ; U; V) = (τ; θ; V′), then Γθ ⊢ U : τ.

Theorem 2.3 (Completeness and Principality of W^{≪}) For all V and Γ, such that V ∩ CoDom(Γ) = ∅, if Γϕ ⊢ U : τ′, then :

1. W^{≪}(Γ; U; V) ≠ false ;

W^{≪}(Γ; U; V) = (τ; θ; V′)

W^{≪}(Γ; U; V) ≜ match U with
f ⇒ if f ∈ Dom(Γ) then

take (τ; V′) = Inst(Γ(f); V) and θ = θ_{ID}

X ⇒ if X ∈ Dom(Γ) then

take (τ; V′) = Inst(Γ(X); V) and θ = θ_{ID}

U_{1} ≀ U_{2} ⇒ let (τ_{1}; θ_{1}; V_{1}) = W^{≪}(Γ; U_{1}; V) in

let (τ_{2}; θ_{2}; V_{2}) = W^{≪}(Γθ_{1}; U_{2}; V_{1}) in let ϕ = mgu(τ_{1}θ_{2} = τ_{2}) in take τ = τ_{2}ϕ and θ = ϕ ∘ θ_{2} ∘ θ_{1} and V′ = V_{2}

P ⇾ U_{1} ⇒ let \overline{X} = FV(P) and \overline{α_{X}} ∈ V_{1} in

let (τ_{1}; θ_{1}; V_{1}) = W^{≪}(Γ, \overline{X:α_{X}}; P; V \ \{\overline{α_{X}}\}) in

let (τ_{2}; θ_{2}; V_{2}) = W^{≪}(Γθ_{1}, \overline{X:α_{X}θ_{1}}; U_{1}; V_{1}) in take τ = τ_{1}θ_{2} ⇾ τ_{2} and θ = θ_{2} ∘ θ_{1} and V′ = V_{2}

U_{1} U_{2} ⇒ let (τ_{1}; θ_{1}; V_{1}) = W^{≪}(Γ; U_{1}; V) in

let (τ_{2}; θ_{2}; V_{2}) = W^{≪}(Γθ_{1}; U_{2}; V_{1}) in let α ∈ V_{2} in let ϕ = mgu(τ_{1}θ_{2} = τ_{2} ⇾ α) in take τ = αϕ and θ = ϕ ∘ θ_{2} ∘ θ_{1} and V′ = V_{2} \ {α}

let P ≪ U_{1} in U_{2} ⇒ let (τ_{1}; θ_{1}; V_{1}) = W^{≪}(Γ; U_{2}; V) in

let \overline{X} = FV(P) and \overline{α_{X}} ∈ V_{1} in

let (τ_{2}; θ_{2}; V_{2}) = W^{≪}(Γθ_{1}, \overline{X:α_{X}}; P; V_{1} \ \{\overline{α_{X}}\}) in let ϕ = mgu(τ_{1}θ_{2} = τ_{2}) in

let (τ_{3}; θ_{3}; V_{3}) = W^{≪}(Γθ_{1}θ_{2}ϕ, \overline{X:Gen(α_{X}θ_{2}ϕ; Γθ_{1}θ_{2}ϕ)}; U_{1}; V_{2}) in take τ = τ_{3} and θ = θ_{3} ∘ ϕ ∘ θ_{2} ∘ θ_{1} and V′ = V_{3}

_⇒ false

Inst(∀\overline{α}.τ; V) ≜ (τ\{\overline{β/α}\}; V \ \{\overline{β}\}) where \overline{β} are distinct fresh variables taken in V

Fig. 4 – The Algorithm W^{≪}.

2. W^{≪}(Γ; U; V) = (τ; θ; V′), for some τ and θ and V′;

3. τ′ = τψ and ϕ =^{V}∢̸ ψ ∘ θ, for some ψ.

Theorem 2.4 (Decidability of Type Inference for rhoStk) The following problems are decidable :

1. Type Inference : for a closed term U such that stk ∉ U, given Γ (such that every constant of U is in Dom(Γ)), find a τ such that Γ ⊢ U : τ.

2. Type Checking : for a closed term U such that stk ∉ U, given Γ and τ′, check that the judgment Γ ⊢ U : τ′ holds.

3. Core ML vs. Core rhoStk

In this section we briefly compare the syntax and semantics of the well-known core ML calculus, at the basis to the ML language, with rhoStk which could be thought as a core calculus for both ML and different rewrite-based languages. Particular focus has been put on the ratio between the theoretical tools we use w.r.t. the language idioms we would like to capture. The ML definitions comes from the tutorial on ML by Remy [Rém02], and the Caml notes by Pottier [Pot].

3.1. Core ML

Core ML is a fragment of ML. We recall the language and the type syntax :

Core ML

τ ::= α | ι | τ ⇾ τ | τ × τ  Poly Types
σ ::= ∀\overline{α}.τ  Poly Type Schemes
M ::= c | x | λx.M | M M | let x = M in M Poly Terms

The operational semantics and the typing rules are the usual ones [Rém02]. Although this fragment is sufficiently expressive, and its type inference system is terminating, sound, and decidable, it lacks of useful language constructs, like recursion. To achieve this one may want to add a fix operator and a let rec operator. This leads to an enriched syntax :

Core ML + fix

τ ::= As before  Poly Types
σ ::= As before  Poly Type Schemes
M ::= As before | fix Poly Terms + Fix

and to new static and dynamic semantics. First, we should add a new rule in the operational semantics

(δ_{fix}) fix f v → f (fix f) v

where v is a term in normal form following the call-by-value strategy.

We assume the following syntactic sugar for let rec

let rec f = λx.M_{1} in M_{2} ≜ let f = fix (λf.λx.M_{1}) in M_{2}

and add the following typing rule for fix

{τ ≡ τ_{1} → τ_{2} \atop Γ ⊢ fix : (τ → τ) → τ} (Fix)

Even if the Core ML + fix fragment is quite expressive, it does not feature explicit matching which has been proved useful in case analysis. This extension is not so complicated : we need to enrich the type-syntax with sum-types and the calculus with appropriate injection and selection operations :

    Core ML + fix + match

τ ::= As before | τ + τ  Poly Types
σ ::= As before  Poly Type Schemes
M ::= As before | inj_{i}^{n} M | match_{n} M M_{1} … M_{n} Poly Terms + Fix + Match

We should also add a new rule in the operational semantics

(δ_{match}) match_{n}(inj_{i}^{n} v) v_{1} … v_{n} → v_{i} v

where all v’s are terms in normal form following the call-by-value strategy, and add the following type rules for inj :

{Γ ⊢ M : τ_{i} \atop Γ ⊢ inj_{i}^{n}M : τ_{1} + … + τ_{n}} (inj) \begin{matrix}Γ ⊢ M : τ_{1} + … + τ_{n} \\ Γ ⊢ M_{i} : τ_{i} → τ & ∀i = 1 … n \end{matrix} Γ ⊢ match_{n} M M_{1} … M_{n} : τ (match)

This extension is morally equivalent to our rhoStk. The computability capabilities are the same, but the latter includes, as built-in features, recursion and pattern matching. This makes rhoStk a suitable candidate as a core calculus that should be more deeply compared w.r.t. the corresponding Core ML

+ fix + match.

4. Conclusions

In this paper we have presented a typed rewriting calculus called rhoStk which features a restricted form of polymorphism à la Damas-Milner-Tofte. We have customized the well-known algorithm W of Damas-Milner [DM82] for the presented calculus and we have proved the classical properties such a system should satisfy : the soundness, completeness, principality of the type inference algorithm, and thus the decidability of the type inference.

We have already shown that reduction strategies in term rewrite systems can be automatically encoded by (untyped) ρ-terms [CLW04]. The type inference algorithm we have presented here gives a correctness criterion for these terms and consequently for the encoded term rewrite system. Starting from the type system proposed in this paper we can also improve the expressiveness of the type systems usually used in rewrite-based languages with polymorphic features. This could be the case for parametric polymorphism as used in ELAN and Maude. Dealing furthermore with sub-typing is a useful open question that we are planning to study.

A useful application that still needs more investigations is to help in checking for the correctness of XML queries using the paradigms, techniques and results presented in this paper. Indeed, XML query languages like Xquery, TOM or Xcerpt (to mention just a few) are based on matching capabilities and the queries are expressed by specific rewrite rules. Of course, it will be most useful to ask the less contextual informations to the user nd to use the DTD or the XML schema together with type inference to help the user in making safer and meaningful queries [CCD^{+}05]. Such investigations are underway in languages like CDUCE [BCF03, HFC05] and we believe that the polymorphic rewriting calculus can bring a useful framework towards the useful interactions of matching and polymorphic types for XML.

Références

[Bar84] H. Barendregt. Lambda Calculus : its Syntax and Semantics. North Holland, 1984.

[BCF03] V. Benzaken, G. Castagna, and A. Frisch. Cduce : an xml-centric general-purpose language. In C. Runciman and O. Shivers, editors, ICFP, pages 51–63. ACM, 2003.

[BCKL03] G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori. Pure Patterns Type Systems. In Proc. of POPL, pages 250–261. The ACM press, 2003.

[BCM04] D. A. Basin, M. Clavel, and J. Meseguer. Reflective metalogical frameworks. ACM Trans. Comput. Log., 5(3) :528–576, 2004.

[Cas96] C. Castro. Solving Binary CSP using Computational Systems. In J. Meseguer, editor, Proceedings of the first international workshop on rewriting logic, volume 4, Asilomar (California), September 1996. ENTCS.

[CCD^{+}05] H. Cirstea, E. Coquery, W. Drabent, F. Fages, C. Kirchner, L. Liquori, B. Wack, and A. Wilk. Types for Rewerse Reasoning and Query Languages. Deliverable, 2005. REWERSE Network of Excellence.

[CKL01a] H. Cirstea, C. Kirchner, and L. Liquori. Matching Power. In Proc. of RTA, volume 2051 of LNCS, pages 77–92. Springer-Verlag, 2001.

[CKL01b] H. Cirstea, C. Kirchner, and L. Liquori. The Rho Cube. In Proc. of FOSSACS, volume 2030 of LNCS, pages 166–180, 2001.

[CLW04] H. Cirstea, L. Liquori, and B. Wack. Rewriting calculus with fixpoints : Untyped and first-order systems. In TYPES’03, volume 3085 of Lecture Notes in Computer Science, Torino, 2004.

[CKLW06] H. Cirstea, C. Kirchner, L. Liquori, and B. Wack. Decidable Type Inference for the Polymorphic Rewriting Calculus. Technical Report inria-00000817, Loria, 2006. Available

at http://hal.inria.fr

[CMR04] H. Cirstea, P.-E. Moreau, and A. Reilles. Rule based programming in java for protocol verification. In Workshop on Rewriting Logic and Applications, Barcelona (Spain), March 2004. Electronic Notes in Theoretical Computer Science.

[Cur34] H. Curry. Functionality in Combinatory Logic. In Proc. Nat. Acad. Sci. U.S.A., volume 20, pages 584–590, 1934.

[DM82] L. Damas and R. Milner. Principal Type-Schemes for Functional Programs. In Proc. of POPL, pages 207–212. The ACM Press, 1982.

[EMS03] S. Eker, J. Meseguer, and A. Sridharanarayanan. The maude ltl model checker and its implementation. In T. Ball and S. K. Rajamani, editors, SPIN, Lecture Notes in Computer Science, pages 230–234. Springer, 2003.

[FN96] K. Futatsugi and A. Nakagawa. An Overview of Cafe Project. In Proc. of CafeOBJ Workshop, 1996.

[Gog04] J. Goguen. The OBJ Family Home Page, 2005.

http://www.cs.ucsd.edu/users/goguen/sys/obj.html.

[GR88] P. Giannini and S. Ronchi della Rocca. Characterization of Typings in Polymorphic Type Discipline. In Proceedings of the Third Annual Symposium on Logic in Computer Science, pages 61–70, 1988.

[HFC05] H. Hosoya, A. Frisch, and G. Castagna. Parametric polymorphism for xml. In J. Palsberg and M. Abadi, editors, POPL, pages 50–62. ACM, 2005.

[JK91] J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras : a rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257–321. The MIT press, Cambridge (MA, USA), 1991.

[KMR05] C. Kirchner, P.-E. Moreau, and A. Reilles. Formal validation of pattern matching code. In PPDP ’05 : Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, pages 187–197, New York, NY, USA, 2005. ACM Press.

[Lei83] D. Leivant. Polymorphic Type Inference. In Proc. of POPL, pages 88–98. The ACM Press, 1983.

[LW05] L. Liquori and B. Wack. The polymorphic rewriting-calculus : Type checking vs. type inference. In N. Martí-Oliet, editor, Proceedings of the Fifth International Workshop on Rewriting Logic and Its Application, volume 117 of entcs, pages 89 – 111. Elsevier B. V., 2005.

[MOM02] N. Martí-Oliet and J. Meseguer. Rewriting Logic : Roadmap and Bibliography. Theoretical Computer Science, 285(2) :121–154, 2002.

[MRV03] P.-E. Moreau, C. Ringeissen, and M. Vittek. A Pattern Matching Compiler for Multiple Target Languages. In G. Hedin, editor, 12th Conference on Compiler Construction, Warsaw (Poland), volume 2622 of LNCS, pages 61–76. Springer-Verlag, May 2003.

[MTHM97] R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

[Pey87] S. Peyton Jones. The Implementation of Functional Programming Languages. Prentice Hall, 1987.

[Pot] F. Pottier. Course DEA : Typage et programmation. http://pauillac.inria.fr/

~fpottier/mpri/dea-typage.ps.gz.

[Rém02] D. Rémy. Using, Understanding, and Unraveling the OCaml Language. In Applied

Semantics. Advanced Lectures. LNCS 2395., pages 413–537. Springer Verlag, 2002.

[Rob65] J. A. Robinson. A machine-oriented logic based on the resolution principle. journal of the ACM, 12 :23–41, 1965.

[Ste02] M.-O. Stehr. Programming, Specification and Interactive Theorem Proving – Towards a Unified Language based on Equational Logic, Rewriting Logic and Type Theory. PhD thesis, Universität Hamburg, Fachbereich Informatik, 2002.

[The03a] The Cristal Team. The Objective Caml Home Page, 2003.

http://www.ocaml.org/.

[The03b] The GNU Prolog Team. The GNU Prolog Home Page, 2003.

http://pauillac.inria.fr/~diaz/gnu-prolog/.

[The04a] The Asf+Sdf Team. The Asf+Sdf Meta-Environment Home Page, 2005. http://www.

cwi.nl/htbin/sen1/twiki/bin/view/SEN1/MetaEnvironment.

[The04b] The Haskell Team. The Haskell Home Page, 2005.

http://www.haskell.org/.

[The04c] The Maude Team. The Maude Home Page, 2005.

http://maude.cs.uiuc.edu/.

[The04d] The Protheo Team. The Elan Home Page, 2005.

http://elan.loria.fr.

[The04e] The Scheme Team. The Scheme Language, 2005.

http://www.swiss.ai.mit.edu/projects/scheme/.

[vdBKV96] M. van den Brand, P. Klint, and C. Verhoef. Core technologies for system renovation. In K. G. Jeffery, J. Král, and M. Bartosek, editors, SOFSEM : Theory and Practice of Informatics, 23rd Seminar on Current Trends in Theory and Practice of Informatics, volume 1175 of Lecture Notes in Computer Science, pages 235–254. Springer, 1996.

[vO90] V. van Oostrom. Lambda Calculus with Patterns. Technical Report IR-228, Faculteit der Wiskunde en Informatica, Vrije Universiteit Amsterdam, 1990.

[Wac05] B. Wack. Typage et déduction dans le calcul de réécriture. Thèse de doctorat, Université Henri Poincaré - Nancy I, Oct 2005.

[Wel99] J. B. Wells. Typability and Type Checking in System F are Equivalent and Undecidable. Annals of Pure and Applied Logic, 98(1–3) :111–156, 1999.

70