Regular Typed Unification
João Barbosa Mário Florido Vítor Santos Costa












Regular Types Unification]Regular Typed Unification


Departamento de Ciência de Computadores, Faculdade de Ciências, Universidade do Porto

Rua do Campo Alegre s/n, 4169–007 Porto, Portugal
LIACC - Laboratório de Inteligência Articial e Ciência de Computadores

Departamento de Ciência de Computadores, Faculdade de Ciências, Universidade do Porto

Rua do Campo Alegre s/n, 4169–007 Porto, Portugal
LIACC - Laboratório de Inteligência Articial e Ciência de Computadores

Departamento de Ciência de Computadores, Faculdade de Ciências, Universidade do Porto

Rua do Campo Alegre s/n, 4169–007 Porto, Portugal
INESCTEC - Instituto de Engenharia de Sistemas e Computadores, Tecnologia e Ciência















[
    Vítor Santos Costa
    
======================

 
Here we define a new unification algorithm for terms interpreted in semantic domains denoted by a subclass of regular types here called deterministic regular types. This reflects our intention not to handle the semantic universe as a homogeneous collection of values, but instead, to partition it in a way that is similar to data types in programming languages.
We first define the new unification algorithm which is based on constraint generation and constraint solving, and then prove its main properties: termination, soundness, and completeness with respect to the semantics. Finally, we discuss how to apply this algorithm to a dynamically typed version of Prolog.


Regular Types, Unification, Typed Unification




§ INTRODUCTION


In mathematical logic, a term denotes a mathematical object. In logic programming this notion is generalized to terms as a syntactic representations of structured data. 
A theory of equality on the set of all terms formally defines which terms are considered equal. In the most typical case of first order theories only syntactically identical terms are considered equal. In this case functions are uninterpreted functions or, computationally, functions build data terms, rather than operating on them. 

When the domain of discourse contains elements of different kinds, it is useful to split the set of all terms (Universe) accordingly. To this end, a type (sometimes also called sort) is assigned to variables and constant symbols, and a declaration of the domain type and range type to each function symbol. A typed term f(t_1,...,t_n) may then be composed from the subterms t_1,...,t_n only if the i-th subterm's type matches the declared i-th domain type of f. Such a term is called well-typed and terms which are not well-typed are called ill-typed.

Previous approaches for types in logic programming use regular types as the type language for logic programming <cit.>.  
A subset of regular types, which restricts individual type definitions to be deterministic, allows for decidable emptiness checking, subset checking, and a intersection and unification operations as defined by Dart and Zobel <cit.>. However, when trying to find a semantic partition corresponding to regular types (even with the same restriction), type checking is not trivial.


Data type definitions in programming languages impose constraints to the type language to allow decidable type checking. Usually data types are possibly recursive definitions where type constructors are unique.
Here we propose a stricter subset of regular types that we shall call deterministic regular types, which corresponds exactly to the restriction mentioned above. In a deterministic regular type each type constructor (here called type function symbol) is unique.

We will focus our attention on equality in a theory where the semantic universe is partitioned in a way consistent with deterministic regular types, similarly to data types in programming languages. More specifically, this paper is concerned with unification in typed first order theories, where types are described by deterministic regular types.

With this motivation in mind we present a term unification algorithm which may now return three different results: a most general unifier, failure or wrong. This last value wrong is inspired by a similar notion used by Robin Milner to denote run-time type errors in functional programs <cit.> and, in our framework, it corresponds to the unification of terms that can never belong to the same semantic domains.

A function now, may map integers to integers, integers to lists, floats to lists of integers, and, thus, the Herbrand universe is now divided in many different domains.


Let cons be the list constructor with type cons :: ∀α. α× list(α) → list(α), where list(α) = [ ] + [α | list(α)] (+ denotes disjoint type union). Suppose we have terms t_1 = cons(1,X) and t_2 = cons(Y,2). These terms unify using first-order (untyped) unification, but they do not have a correct type, since the second argument of cons must be a list. This ill-typing is captured by our new typed unification algorithm that, in this case, outputs wrong.


Related Work This paper generalizes a typed unification algorithm previously defined by the authors in <cit.> that was used in the dynamic typing of logic programs. In <cit.> functions symbols f of arity n had co-domains which were always sets of terms of the form f(t_1,…,t_n), where the arguments t_i belong to the corresponding domain of f. This basically induced a partition of the Herbrand domain into sets of trees. Here we extend this notion enabling the use of semantic domains and co-domains described by deterministic regular types. 

The most obvious related work is many-sorted unification <cit.>, though many-sorted unification assumes an infinite hierarchy of sorts and we do not assume a hierarchy of types. In particular there is a relation with many-sorted unification with a forest-structured sort hierarchy <cit.>, but even compared with this strong restricted unification problem, our work gives easier and nicer results, mostly due to the use of an expressive universe partition based on deterministic regular types but with no underlying hierarchy on the domains.  

Here we study unification of terms interpreted in domains described by deterministic regular types, and we allow a form of parametric polymorphism in the description of term variables. Parametric polymorphic descriptions of sorted domains goes back to Smolka generalized order-sorted logic <cit.>. In his system, subsort declarations are propagated to complex type expressions, thus the main focus is on subtyping which is not the scope of our work.

Contributions Our main contributions are: an extension to the semantics defined in <cit.>, where equality takes into account the domains of the two terms in the left and the right hand side of an equation, being wrong when terms belong to disjoint domains; a type system for terms and the equality predicate which we prove to be sound with respect to the semantic typing relation; and a new unification algorithm, which given an equation between two terms returns their most general unifier and their principal type, if there is a solution, false if there is not a solution but terms can belong to the same semantic domain and wrong otherwise. 

This three stage framework (first a notion of semantic typing, then a type system for terms and equations which is sound with respect to semantic typing and, finally, a unification algorithm which is sound and complete with respect to the type systems) enables to smoothly prove soundness and completeness of our unification algorithm, and it is inspired by the type theory in Milner <cit.> where he also defined a notion of semantic typing, then a type system which was sound with respect to semantic typing and a type inference algorithm which was sound and complete with respect to the type system.


















































§ TERM SYNTAX AND SEMANTICS


We will, firstly, define the language of terms. For a more in detail presentation, we refer the reader to <cit.>.

Given an infinite set of variables VAR and an infinite set of function symbols FUNC, a term is:

    
  * a variable (, , , …);
    
  * a function symbol of arity 0 (, , , , …), which we call a constant;
    
  * a function symbol of arity n≥1 (, , , …) applied to an n-tuple of terms.


We call terms that contain no variables ground terms, and terms that start with a function symbol with arity n≥1 complex terms.

Following the standard Herbrand interpretation of logic programs <cit.>, we assume that every term represents a tree and that all these trees are part of the universe of interpretation of the logic program.

Any division of the universe leads to a typed unification algorithm, but here, we assume a particular partition of the universe into several domains. Note that this interpretation just groups sets of trees in the universe into domains, and includes some other domains that are not consisting of trees. Thus, here we divide the universe U into domains as follows:


    𝐔 = 𝐈𝐧𝐭∪𝐅𝐥𝐭∪𝐒𝐭𝐫∪𝐀𝐭𝐦∪𝐋𝐢𝐬𝐭_1∪…∪𝐋𝐢𝐬𝐭_𝐧∪𝐀_1∪…∪𝐀_𝐦∪𝐁𝐨𝐨𝐥∪𝐅∪𝐖𝐫𝐨𝐧𝐠,


where Int is the set of trees that represent integers (examples include  and , but also trees such as  and ), Flt is the set of trees that represent floating-point numbers (similarly to Int, we consider every tree that represents a floating-point number, including trees whose root is an arithmetic operator), Str is the set of trees representing strings, Atm is the set of trees consisting of a single node, the root, that are not included in any other domain, 𝐋𝐢𝐬𝐭_𝐢 are sets of trees that represent lists, where each domain contains the trees that represent lists of elements of some other domain (i.e., we have a domain for lists of integers, lists of strings, lists of lists of integer, …), 𝐀_𝐢 are the domains of trees whose root is a function symbol and the nodes of each tree are in the same domain as the corresponding nodes of every other tree (examples: f(Int), g(Int, Float), h(g(Atom),h(Int)), …), Bool is the set with true and false, F is the set of semantic functions, and Wrong is the set with a single value, wrong. We call base domains to the domains Int, Flt, Str, and Atm.

One important note here is the value , corresponding to the empty list. We assume that this value belongs to every list domain, and that it is the only value that belongs to more than one domain in this partition.

Then, the semantics of a term is a tree in some domain, or wrong. The semantics depends on an interpretation I for the function symbols in the language, and a state Σ which associates variables to semantic values. We assume that the value returned by I is, for constants, a tree with just a root, and for function symbols of arity n≥1 a function in F, that outputs a tree and has as input some domains. We assume that, for all function symbols  except the list constructor , the corresponding function in I is a function f that has signature f : ∀α_1,…,α_n. α_1 ×…×α_n → f(α_1,…,α_n), such that if any of the arguments the function is applied to is wrong then it outputs wrong, otherwise it outputs the tree with root f and children the trees it got has input. For the list constructor  the function associated in I is cons with signature cons : ∀α. α× list(α) → list(α) defined as:

    (v_1,v_2) =
        
          cons(v1,v2)    if v_1 ∈ D ∧ v_2 ∈ List(D)
    
          wrong    otherwise


The predefined interpretation I is the one where every constant has the expected value, for instance the term 1 has as value the integer , and the term a has as value the atom . One additional useful definition is the function dom that returns what is the domain of a value.

We define the semantics of a term, represented by |[ |]_I,Σ, in the following way:

    
  * |[X|]_I,Σ = Σ(X)
    
  * |[k|]_I,Σ = I(k)
    
  * |[f(t_1,…,t_n)|]_I,Σ = I(f) (|[t_1|]_I,Σ,…,|[t_n|]_I,Σ)


Note that, if a complex term contains the list constructor, the semantics of that term can be wrong. This is where the division into domains comes into play, since if we were considering an undivided Herbrand universe, then trivially all values are in the same domain so the application of a function could never generate an error. This is not realistic in any typed programming language, but also true for untyped languages: note that Prolog, the main logic programming language, already includes some division of the universe into values, implicit by the use of type predicates such as integer, float or atom.



We assume one predicate, equality, hereby represented by =. The semantics of equality is re-adjusted to take into account the value wrong. Equality is defined for terms in the same domain. So let function eq with signature eq :∀α. α×α→ Bool be defined as follows:

    eq(v_1,v_2) =
        
          true    if v_1 = v_2 ∧ dom(v_1) ∩ dom(v_2) ≠∅∧ dom(v_1) ≠ Wrong
    
          false    if v_1 ≠ v_2 ∧ dom(v_1) ∩ dom(v_2) ≠∅∧ dom(v_1) ≠ Wrong 
    
          wrong    otherwise


The semantics for the equality predicate is then as follows:

|[t_1 = t_2|]_I,Σ = eq(|[t_1]_I,Σ,|[t_2|]_I,Σ)

Note that there are two ways of returning wrong in an equality: either one of the terms contains an error in itself (i.e., has the semantic value wrong), therefore it belongs to the domain Wrong, or the semantics for the terms belongs to domains with an empty intersection. The second case needs some explanation. We could define it as dom(v1) ≠ dom(v2), but for values that belong to several domains, such as , the dom function returns the union of all the domains, so equality is well defined when one finds a common domain for both terms.










§ TYPE LANGUAGE


Here we define a syntactic description of semantic domains. This syntactic description corresponds to the well know concept of a type. The alphabet for the language of types includes an infinite set of type variables TVar, a finite set of base types TBase, an infinite set of type function symbols TFunc, an infinite set of type symbols TSym, parenthesis, and the comma. There is a one-to-one correspondence between TFunc and Func, which we assume is predefined.
Then, we have the following grammar for types:



all_type      ::=     cons_type | func_type

cons_type     ::=     type | type_term

func_type     ::=     type_1 ×…× type_n → type

type           ::=     tvar | tbase | tsymbol(type_1,…,type_n)

type_term     ::=     tconstant | tfunction(cons_type_1,…,cons_type_n)

type_def      ::=     tsymbol(tvar_1,…,tvar_n) –> type_term_1 + … + type_term_m



Where tvar ∈ TVar, tbase ∈ TBase, tconstant, tfunction ∈ TFunc, and tsymbol ∈ TSym. We call a type term that starts with a tfunction a complex type term. We call ground to any type that does not contain a type variable. 

Each type symbol is defined by a type definition. A well-formed type definition has all tvar that occur as parameters on the left-hand side of the definition, occurring somewhere on the right-hand side. The sum τ_1 + … + τ_n is a union type, describing values that have one of the type terms τ_1,…,τ_n, called the summands. The `+' is an idempotent, commutative, and associative operation.

A set of type definitions D is called deterministic if any type function symbol 
occurs at most once in D. Note that in a deterministic set of type definitions no two type terms on the right-hand side of a definition have the same principal functor. Deterministic type definitions include tuple-distributive types <cit.> and correspond to the widely used algebraic data types in programming languages. From now on we assume that type definitions are deterministic and well-formed.

A type scheme σ is either a type, a functional type or an expression of the form ∀α_1,…,α_n.τ, where τ is an all_type and α_1,…,α_n are type variables which will be called the generic variables of σ. Note that types form a subclass of type schemes. To simplify presentation, we will often abbreviate type schemes to ∀α⃗.τ, where α⃗ denotes a sequence of several type variables α_i. Type
 schemes represent parametric polymorphic types <cit.>.





§ SEMANTICS

Each type is associated with a domain. A base type tbase is associated with a base domain, and each instance of a type of the form tsymbol(type_1,…,type_n) is associated with a domain. In our language we include a single type symbol list that is associated with the domains for lists. We assume that the definition for the type symbol list is: list(α) –> [ ] + cons(α,list(α)). We could include further type symbols that were defined by inductive definitions, such as lists, and the rest of this paper could be easily extended to include different inductively defined types, but we keep list as the only one in this paper for the sake of simplicity. We assume that every type term on the right-hand side of a type definition is a type constant or a complex type term, and the definitions are deterministic (each type constant and type function symbol occurs only once). 

A valuation ψ gives a ground type for each type variable. Formally, the semantics of a type is a domain. Given a valuation ψ, we define the semantics of a type as follows:


𝐓|[α|]_ψ = 𝐓|[ψ(α)|]_ψ

𝐓|[int|]_ψ = Int

𝐓|[float|]_ψ = Flt

𝐓|[string|]_ψ = Str

𝐓|[atom|]_ψ = Atm

𝐓|[list(α)|]_ψ = 𝐓|[list(ψ(α))|]_ψ

𝐓|[list(int)|]_ψ = List(Int), same for any other ground instance of list(α)
 
The semantics of a type_term is as follows, also given a valuation ψ:

𝐓|[k|]_ψ = {k}

𝐓|[f(τ_1,…,τ_n)|]_ψ = { f(v_1,…,v_n) | v_i ∈𝐓|[τ_i|]_ψ}


The semantics of a union_type, given a valuation ψ, is:

𝐓|[τ_1 + … + τ_n|]_ψ = 𝐓|[τ_1|]_ψ∪…∪𝐓|[τ_n|]_ψ


The semantics of a func_type, given a valuation ψ, is:

𝐓|[τ_1 ×…×τ_n →τ|]_ψ = 
{ f | f ∈𝐅∧∀ v_1 ∈𝐓|[τ_1|]_ψ,…,v_n ∈𝐓|[τ_n|]_ψ. f(v_1,…,v_n) ∈𝐓|[τ|]_ψ}


And, finally, the semantics of a type scheme is:

𝐓|[∀α⃗.τ|]_ψ = ⋂_∀σ⃗𝐓|[τ[α⃗↦σ⃗]|]_ψ, where σ⃗ is a sequence of types of the same size as α⃗.


Note that the semantics of a (ground) type_term may be a domain, as in the case of f(int,float), or the subset of a domain, as in the case of cons(int,[ ]), or even a subset of several domains, as in the case of [ ]. This includes a subset of the domain Wrong, as in the case of cons(int,int). All instances of complex type terms whose tfunction is not the list constructor are associated with a domain for trees.

Also note that we assume a function, given by I, for the interpretation of function symbols, thus functions have type signatures: the type of a function symbol f of arity n is interpreted as function which builds a tree of root f, with the type scheme ∀α_1,…,α_n. α_1 ×…×α_n → f(α_1,…,α_n). The semantics for this type scheme is the intersection of the semantics for all instances of the functional type, which is a subset of F consisting of all functions that have such type. So it consists of all the functions that can have any tuple of n elements as input and output a tree whose root is f and the children nodes are the input elements.






 §.§ Semantic Typing




We now define what it means for a term to semantically have a type, denoted by t : τ. If the term and the type are both ground, given an interpretation I, we just check whether the semantics of the term belongs to the domain corresponding to the semantics of the type. So, for ground terms and types:


    t : τ∀Σ.∀ψ. |[t|]_I,Σ∈𝐓|[τ|]_ψ


However, both terms and types can be non-ground in general and, without extra information, we cannot know what is the correct type for a variable. To deal with variables we introduce the concept of a context Γ, where we have typings of the form X : τ for variables. Now, given a context associating variables with types, we are able to define the semantic typing relation, denoted by ⊩, defined as:


    Γ⊩_I t:τ∀Σ.∀ψ. (∀ (X:τ') ∈Γ. |[X|]_I,Σ∈𝐓|[τ'|]_ψ  |[t|]_I,Σ∈𝐓|[τ|]_ψ)


Contexts allow us to type non-ground terms, assuming that the types for each variable are the ones given in the context. So the same term may have different types depending on the context, if it is non-ground (since ground terms always have the same type, due to the nonexistence of variables in the term that depend on the context). We call the generic context to the context that contains X_i : α_i, for all variables, i.e., all variables have the most general type they can have, a type variable, and each type variable is associated with a particular term variable.


Let Γ = {:α, : list(α)} and Δ = { : ∀α. α× list(α) → list(α)}.

    Γ,Δ_I : list(α)

Suppose we have a state Σ and a valuation ψ such that |[|]_I,Σ∈𝐓|[α|]_ψ and |[|]_I,Σ∈𝐓|[list(α)|]_ψ, then |[  |]_I,Σ∈𝐓|[list(α)|]_ψ. Since |[|]_I,Σ = Σ(X) ∈𝐓|[ψ(α)|]_ψ and |[|]_I,Σ = Σ(Y) ∈𝐓|[ψ(list(α))|]_ψ, by the semantics of , we have cons(Σ(X),Σ(Y)), which is not wrong from the domains of the respective values, and because the output is in the correct domain.

However, note that for Γ' = {:α, : β}, the same would not be true, since for Σ = [X ↦ 1, Y ↦ 2] and ψ = [α↦ int, β↦ int], the left-hand side of the implication is true, but cons(1,2) (= wrong) ∉𝐓|[list(Int)|]_ψ.




§ SYNTACTIC TYPING


This section introduces syntactic typing by the definition of a type system for terms and the equality predicate.
A context Γ and a set of type assumptions for constants and function symbols Δ are needed to derive a type assignment and one writes Γ,Δ⊢ t:τ (pronounce this as Γ and Δ yield t in τ).
Assumptions in Δ are of the form k:∀α⃗.τ, for constants, and f : ∀α⃗.τ_1×…×τ_n →τ, for function symbols, where the generic variables α⃗ of these type schemes are exactly the type variables that occur in τ and τ_1 ×…×τ_n →τ, respectively. 

A statement t:τ is derivable from contexts Γ and Δ, notation Γ,Δ⊢ t:τ, if Γ,Δ⊢ t:τ can be produced by the following rules.




The type system definition pays particular attention to the mode of the typing judgment. In particular, the type contexts and term are interpreted as inputs to the typing judgment, while the term’s type is viewed as an output.

We must guarantee that Δ is in agreement with I. For this, we have the following relation: Sig_I⊩Δ, which is defined as ∀ (k : τ) ∈Δ. dom(I(k)) = τ∧∀ (f : τ_1 ×…×τ_n →τ). I(f) : τ_1 ×…×τ_n →τ. We purposefully overload the symbol ⊩ since this corresponds to a semantic validation of a syntactic typing.


Let Γ = {X : int, Y : list(int)}, Δ = {1 : int, nil : ∀γ. list(γ), cons : ∀β. β× list(β) → list(β)}, and Λ = (cons : ∀β. β× list(β) → list(β) ) ∈Δ. Then the following type derivation holds using the type rules:


*[]
   * []
    
        *[]
        (X : int)∈Γ
        Γ, Δ⊢X : int
            
        *[]
        ([ ] : ∀γ. list(γ)) ∈Δ
        Γ, Δ⊢[ ] : list(int)^(2)
          
        Λ
    Γ, Δ⊢cons(X,[ ]): list(int)^(1)
        
    * []
    
        *[]
        (1 : int) ∈Δ
        Γ, Δ⊢1 : int
            
        *[]
        (Y : list(int)) ∈Γ
        Γ, Δ⊢Y : list(int)
          
        Λ
    Γ, Δ⊢cons(1,Y): list(int)^(2) 

 Γ, Δ⊢cons(X,[ ]) = cons(1,Y): bool 

Note that in ^(1) we used list(β)[β↦ int] and in ^(2) we used list(γ)[γ↦ int]. Also note that if X : α instead of X:int was in Γ, we could not have a derivation.


We now prove that the rules for syntactic typing are sound, that is, if the set Δ is in agreement with I, then any type derivation is semantically correct.


If Γ, Δ⊢ t:τ and Sig_IΔ, then Γ⊩_I t:τ.



We will prove this by induction on the derivation.

    
  * If the term t is a variable X, then the derivation consists of a single application of axiom VAR. Clearly, it is also true that Γ⊩_I X:τ, where (X:τ) ∈Γ, since any Σ that gives values to X and ψ that gives values to τ, such that |[X|]_I,Σ∈𝐓|[τ|]_ψ will do so in the context and in the term itself simultaneously, so Γ⊩_I X : τ.

    
  * If the term t is a constant k, then the derivation consists of a single application of axiom CST. Since Sig_IΔ, dom(I(k)) = ∀α⃗.τ, where (k : ∀α⃗.τ) ∈Δ, then k ∈𝐓|[∀α⃗.τ|]_ψ, for any ψ. But since 𝐓|[∀α⃗.τ|]_ψ = ⋂_∀σ⃗𝐓|[τ [α⃗↦σ⃗]|]_ψ, then k ∈𝐓|[τ [α⃗↦σ⃗]|]_ψ. So for any Σ, the right-hand side of the implication is always true, so Γ⊩_I k : τ [α⃗↦σ⃗].

    
  * If the term t is a complex term f(t_1,…,t_n), then we can assume, by induction hypothesis, that Γ, Δ⊩ t_i: τ_i[α⃗↦σ⃗], for all i = 1,…,n. Since Sig_IΔ, I(f): ∀α⃗. τ_1 ×…×τ_n →τ, then f ∈𝐓|[∀α⃗. τ_1 ×…×τ_n →τ|]_ψ, for all ψ, so f ∈𝐓|[(τ_1 ×…×τ_n →τ)[α⃗↦σ⃗]|]_ψ. Therefore, we know that, if v_i ∈𝐓|[τ_i[α⃗↦σ⃗]|]_ψ then f(v_1,…,v_n) ∈𝐓|[τ[α⃗↦σ⃗]|]_ψ. For any Σ and ψ such that ∀ (X:τ') ∈Γ. |[X|]_I,Σ∈𝐓|[τ'|]_ψ, 
    we know by the induction hypothesis |[t_i|]_I,Σ∈𝐓|[τ_i[α⃗↦σ⃗]|]_ψ. Therefore, for the same Σ and ψ, we know that |[f(t_1,…,t_n)|]_I,Σ∈𝐓|[τ[α⃗↦σ⃗]|]_ψ, so Γ⊩_I f(t_1,…,t_n) : τ[α⃗↦σ⃗].
    
    
  * If we have an equality of two terms t_1 = t_2, we can assume, by induction hypothesis, that Γ⊩_I t_1: τ and Γ⊩_I t_2: τ. Therefore we know that for any Σ and ψ such that ∀ (X:τ') ∈Γ. |[X|]_I,Σ∈𝐓|[τ'|]_ψ, we have |[t_1|]_I,Σ∈𝐓|[τ|]_ψ and |[t_2|]_I,Σ∈𝐓|[τ|]_ψ. So for these Σ and ψ, we have |[t_1 = t_2|]_Σ∈ |[bool|]_ψ. Therefore, Γ⊩_I t_1 = t_2 : bool.



The fact that we have a context that gives the type for each variable raises some interesting questions: is there a preferred context for each term? And, given a term t is there a typing representing all possible typings of t?
An answer to these questions is related with the notion of principal typing <cit.>, which we define here appropriate to our system:


A principal typing is a pair (Γ,τ), such that Γ, Δ⊢ t:τ and for every other pair (Γ',τ') such that Γ', Δ⊢ t : τ', there is a type substitution μ such that μ(Γ) = Γ' and μ(τ) = τ'.


Note that it is not always the case that the context in a principal typing is a generic context.

Let t =. A principal typing for t is ({X : α, Y : list(α)}, list(α)). Note that any renaming of type variable α defines another principal typing, because principal typings are unique up to renaming of type variables. Also note that the type for Y cannot be a type variable, this, in this example, the context is not generic.










§ CONSTRAINTS


While this type system specification has great appeal, the question arises as to whether it can be effectively type checked. Indeed it can by an easy recursive implementation of the type rules. We desire even more flexibility than the language provides as it is. To do so, we generalize the problem beyond purely elided type annotations.
To check implicit types during unification, we must deduce types that are not present in equality equations. To represent this problem in a broader context, we introduce the notion of type constraint which we add to the usual term unification problem.

There are two kinds of constraints. Equality constraints between terms t_1 = t_2, and equality between types τ_1 ≐τ_2. We are here using the same symbol for equality constraints and the equality predicate. We argue that the uses are clear from the context.

We say that a set of equality constraints is in normal form if all constraints are of the form X_i = t_i, for some term t_i, and there is no other occurrence of any X_i that is on the left-hand side of a constraint anywhere else in the set.

A set of equality constraints in normal form can be interpreted as a substitution. We can interpret every constraint of the form X_i = t_i as a substitution of the form [X_i ↦ t_i].

A set of type equality constraints is in normal form if all constraints are of the form α_i ≐τ_i, for some type τ_i, and there is no other occurrence of any α_i on the left-hand side of a constraint anywhere else in the set.

A set of type equality constraints in normal form can be interpreted as a type substitution. We can interpret every constraint of the form α_i ≐τ_i as a type substitution of the form [α_i ↦τ_i].


A substitution θ (or type substitution μ) is called a unifier for terms t_1 and t_2 (or types τ_1 and τ_2), iff θ(t_1) ≡θ(t_2) (or μ(τ_1) ≡μ(τ_2)). Terms t_1 and t_2 (or types τ_1 and τ_2) are unifiable iff there exists a unifier for them.


Our constraints are supposed to represent equality, either of terms or types. However, in the semantics, we need states and valuations to interpret non-ground terms and types, respectively. We need a way to interpret the constraints semantically, so we define the following.


Let c be a constraint, Σ a state, and ψ a valuation. We say that Σ and ψ model c, and represent it by Σ,ψ c if:

    
  * c is an equality constraint of the form t_1 = t_2, then Σ(t_1) ≡Σ(t_2);

    
  * c is a type equality constraint of the form τ_1 ≐τ_2, then ψ(τ_1) ≡ψ(τ_2);



We can know extend this definition to a set of constraints.


Let C be a set of equality constraints and S be a set of type equality constraints. We say that a state Σ and a valuation ψ model the pair (C,S), and represent it by Σ,ψ C,S iff Σ and ψ model all constraints in both sets.


 We now provide an auxiliary definition that relates substitutions and states and use this definition to extend our notion of constraint modelling.


We say that a state Σ follows a substitution θ and represent it by Σ∼θ iff for any term t, |[t|]_I,Σ = v and |[μ(t)|]_I,Σ = v. Similarly, a valuation ψ follows a substitution for types μ (ψ∼μ) iff for any type τ, 𝐓|[τ|]_ψ = 𝐓|[μ(τ)|]_ψ.





Let C be a set of equality constraints and S be a set of type equality constraints. We say that a substitution θ and a type substitution μ model the pair (C,S), and represent it by θ,μ C,S, iff for every state Σ and valuation ψ we have that Σ∼θ∧ψ∼μΣ,ψ C,S.




§ TYPED UNIFICATION ALGORITHM


The typed unification algorithm performs unification on both the terms given as input and the types for those terms. The intuition is that if the types do not unify, then there is a type error. We will prove this condition in the next section.
We follow the approach of <cit.>: generate constraints for typability and solve them. 



 §.§ Constraint Generation


Guided by the definition of our type system we now define a constraint typing judgment, which indicates what constraints must hold for a particular type term-and-context pair to be typable.
Let Γ be a generic context. We use the following rules to generate constraints for the unification of two terms t_1 and t_2. The generated constraints will be the pair (C,T) in Γ⊢ t_1 = t_2 : bool  | C | T. In the rules in Figure <ref>, β⃗ represents a sequence of fresh type variables of the same size of α⃗ in the corresponding case.





Let Γ be a generic context (we will denote the type variable associated with each variable X by α_X), Δ = {1 : int, [ ] : ∀α. list(α), cons : ∀β. β× list(β) → list(β)}, C = {cons(X,[ ]) = cons(1,Y)}, and Λ = (cons : ∀β. β× list(β) → list(β)) ∈Δ. The following constraint type judgements hold:


*[]

    *[]
    (X : α_X)∈Γ
    Γ, Δ⊢X : α_X | ∅ | ∅
        
    *[]
    ([ ] : ∀α. list(α)) ∈Δ
    Γ, Δ⊢[ ] : list(γ) | ∅ | ∅
      
    Λ
Γ, Δ⊢cons(X,[ ]): list(ν) | ∅ | {α_X = ν, list(γ) = list(ν)} (= T_1)


* []

    *[]
    (1 : int) ∈Δ
    Γ, Δ⊢1 : int | ∅ | ∅
        
    *[]
    (Y : α_Y) ∈Γ
    Γ, Δ⊢Y : α_Y | ∅ | ∅
      
    Λ
Γ, Δ⊢cons(1,Y): list(η) | ∅ | {int = η, α_Y = list(η)} (= T_2) 


*[]

    Γ, Δ⊢cons(1,Y): list(η) | ∅ | T_1
        
    Γ, Δ⊢cons(X,[ ]): list(ν) | ∅ | T_2

 Γ, Δ⊢cons(X,[ ]) = cons(1,Y): bool  |  C |  T_1 ∪T_2 ∪{list(ν) = list(η)}    




We will now prove that constraint generation is sound, i.e., if we generate constraints (both equality and type equality constraints), any model for them applied to Γ and the type τ is derivable in the syntactic typing system.


If Γ,Δ⊢ t:τ | C | T and μ T, then μ(Γ), Δ⊢ t : μ(τ) is derivable in the type system.







We will prove this theorem by induction on the derivation.

    
  * If t is a variable X, then we have Γ, Δ⊢ X : α | ∅ | ∅. Any type substitution μ is such that μ∅. And, for any μ, since μ(α) will be the same in Γ and in the consequent of the rule, μ(Γ), Δ⊢ X : μ(α) is derivable in the syntactic typing system by a single application of rule VAR.

    
  * If t is a constant k, then we have Γ, Δ⊢ k : τ[α⃗↦β⃗]  | ∅ | ∅, where (k : ∀α⃗. τ) ∈Δ. Any type substitution μ is such that μ∅. Then, for any such μ we can have the derivation in the syntactic system using a single application of rule CST, using μ(τ[α⃗↦β⃗]) = τ[α⃗↦μ⃗(⃗β⃗)⃗].

    
  * If t is a complex term f(t_1,…,t_n), then we have Γ, Δ⊢ f(t_1,…,t_n) : τ[α⃗↦β⃗]  | ∅ | T_1 ∪…∪ T_n ∪{τ'_1 ≐τ_1[α⃗↦β⃗], …, τ'_n ≐τ_n[α⃗↦β⃗] }, given Γ,Δ⊢ t_i: τ_i' | ∅ |  T_i, for i = 1,…,n. We also know that μ T_1 ∪…∪ T_n ∪{τ'_1 ≐τ_1[α⃗↦β⃗], …, τ'_n ≐τ_n[α⃗↦β⃗] }, and any such μ is such that μ T_i and μτ'_i ≐τ_i[α⃗↦β⃗], for each i = 1,…,n. By the induction hypothesis, we have μ(Γ), Δ⊢ t_i : μ(τ'_i). But we know that μ(τ'_i) = μ(τ_i[α⃗↦β⃗]), since μτ'_i ≐τ_i[α⃗↦β⃗], for all i = 1,…,n. So we also have μ(Γ), Δ⊩ t_i : μ(τ_i[α⃗↦β⃗]). Therefore, by a single application of the CPL rule, we get μ(Γ), Δ⊩ f(t_1,…,t_n) : μ(τ[α⃗↦β⃗]).

    
  * If t is an equality t_1 = t_2, then we have Γ, Δ⊢ t_1 = t_2 : bool  | {t_1 = t_2} | T_1 ∪ T_2 ∪{τ_1 ≐τ_2}, given Γ,Δ⊢ t_1: τ_1' | ∅ |  T_1 and Γ,Δ⊢ t_2: τ_2' | ∅ |  T_2. We also know that μ T_1 ∪ T_2 ∪{τ_1 ≐τ_2}, and any such μ is such that μ T_1, μ T_2, and μτ_1 ≐τ_2. By the induction hypothesis, we have μ(Γ), Δ⊢ t_1 : μ(τ_1) and μ(Γ), Δ⊢ t_2 : μ(τ_2), but since μτ_1 ≐τ_2, we know that μ(τ_1) ≡μ(τ_2). So by a single application of rule EQU, we get μ(Γ), Δ⊢ t_1 = t_2 : μ(bool), and μ(bool) = bool.





 §.§ Constraint Solving


In this section we present a procedure that generalizes unification <cit.> to account for type constraints and produces solutions, where possible. Since each rule simplifies the constraints, together they induce a straightforward decision procedure for type and term constraints.

Suppose we want to unify two terms t_1 and t_2. Let us have Γ⊢ t_1 = t_2 : bool  | C |  T derived in the constraint generation step. Then we apply the following rewriting rules to the tuple (C,T), until none applies. The rules for the rewriting system are meant to be applied in order, i.e., if rule n and n+k can both be applied, we apply n. They are as follows:


    
    
  * (C, {f(τ_1,…,τ_n) ≐ f(τ'_1,…,τ'_n)}∪ Rest) → (C, {τ_1 ≐τ'_1,…,τ_n ≐τ'_n}∪ Rest)
    
  * (C, {τ≐τ}∪ Rest) → (C, Rest)
    
  * (C, {f(τ_1,…,τ_n) ≐ g(τ'_1,…, τ'_m)}∪ Rest) → wrong, if f ≠ g or n ≠ m
    
  * (C, {τ≐α}∪ Rest) → (C, {α≐τ}∪ Rest), τ is not a type variable
    
  * (C, {α≐τ}∪ Rest) → (C, {α≐τ}∪ Rest[α↦τ]), if α does not occur in τ
    
  * (C, {α≐τ}∪ Rest) → wrong, if α occurs in τ

    
    
  * ({f(t_1,…,t_n) = f(s_1,…,s_n)}∪ Rest,T) → ({t_1 = s_1,…,t_n = s_n}∪ Rest,T)
    
  * ( {t ≐ t}∪ Rest,T) → (Rest,T)
    
  * ({f(t_1,…,t_n) = g(s_1,…,s_m)}∪ Rest,T) → false, if f≠ g or n ≠ m
    
  * ({t≐ X}∪ Rest,T) → ({X ≐ t }∪ Rest,T), t is not a variable
    
  * ({X≐ t}∪ Rest,T) → ({X ≐ t}∪ Rest[X ↦ t],T), if X does not occur in t
    
  * ({X≐ t}∪ Rest,T) → false, if X occurs in t.



Let  C = {cons(X,[ ]) = cons(1,Y)} and T = {α_X = ν, list(γ) = list(ν), int = η, α_Y = list(η), list(ν) = list(η)}. Step-by-step the algorithm rewrite the pair (C,T) as follows:

(C,T) → (C,{α_X = ν, γ = ν, int = η, α_Y = list(η), list(ν) = list(η)}) →

(C,{α_X = ν, γ = ν, int = η, α_Y = list(η), ν = η}) →

(C,{α_X = ν, γ = ν, η = int, α_Y = list(η), ν = η}) →

(C,{α_X = ν, γ = ν, η = int, α_Y = list(int), ν = int}) →

(C,{α_X = ν, γ = int, η = int, α_Y = list(int), ν = int} ( = T')) →

({X = 1,[ ] = Y},T') → ({X = 1,Y = [ ]},T')

Note that, in the final pair, no more rules apply and we can interpret this pair as a pair of substitutions for terms and for types, respectively.




 §.§ Properties of the Regular Typed Unification Algorithm


There are several important properties of our algorithm. Firstly, it always terminates. Secondly, it is correct, meaning that the result is the same as we would have gotten in the equality theory defined for = semantically. One big obstacle for this second property is that terms may not be ground when we want to unify them, and semantically we always need a state to evaluate variables. We will be conservative and assume that if there is a possible state for which the terms have values in the same semantic domain, then there is no type error (yet). Similarly, if there is a state for which the terms have the same semantic value, then the result is not false (yet).

Here we show that, for any input, the unification algorithm always terminates.


Let (C,T) be the pair of sets of constraints generated for terms t_1 and t_2. The rewrite system always terminates, returning a pair of unifiers, false, or wrong.



We divide the algorithm in two parts. The first consists of the rules 1 to 6, and the second of the rules 7 to 12.
Each of these parts are the Martelli-Montanari algorithm <cit.> for its corresponding kind of constraints, type equality and equality, respectively. Therefore they terminate.

For a formal proof for the termination of the Martelli-Montanari algorithm, we defer the reader to <cit.>.

Moreover, if the Martelli-Montanari terminates, the output is either a most general unifier, or the algorithm fails. In the first part, failure is represented by wrong, and in the second part, it is represented by false. So our algorithm either terminates and outputs wrong, false, or both parts succeed and the algorithm outputs a pair of most general unifiers.


We now know that the algorithm terminates, and what the outputs might be. We will additionally prove that the result is semantically valid. We start by proving a few auxiliary lemmas.


Let (C,T) → (C',T') be a step in the typed unification algorithm, such that the output is not false nor wrong. Then, if for all equality constraints (t_1 = t_2) ∈ C' the substitution θ is a unifier of t_1 and t_2, then θ is also a unifier of each equality constraint in C. Same applies to T' and T, with a type substitution μ.



We will prove this by case analysis.

    
  * C' and C are equal so, trivially, any substitution θ that unifies each equality constraint in C also unifies each equality constraint in C'. Now suppose that μ is a type substitution such that μ(τ_i) = μ(τ_i'), for i = 1,…,n, then, also μ(f(τ_1,…,τ_n)) = μ(f(τ'_1, …, τ'_n)). All other type equality constraints in T are also in T', so any unifier of T' is a unifier of T.

    
  * C' and C are equal so, trivially, any substitution θ that unifies each equality constraint in C also unifies each equality constraint in C'. All type equality constraints in T' are also in T, so all unifiers of T' are unifiers of that subset of T. Moreover, T has one more type equality constraint τ≐τ, but any substitution, in particular any unifier of T' is also a unifier of τ with itself.

    
  * This case does not apply, since the output is wrong.

    
  * C' and C are equal so, trivially, any substitution θ that unifies each equality constraint in C also unifies each equality constraint in C'. Any unifier of T' is also a unifier of T, since swapping the terms on a type equality constraints does not change the fact that a substitution is a unifier.

    
  * C' and C are equal so, trivially, any substitution θ that unifies each equality constraint in C also unifies each equality constraint in C'. Suppose μ is a unifier of T', then μ(α) = μ(τ). Therefore, since T' = T[α↦τ] for all constraints except α = τ, then μ(T') = μ(T[α↦τ]) = (μ∘ [α↦τ])(T) but since μ(α) = μ(τ), then (μ∘ [α↦τ])(T) = μ(T). So μ is also a unifier of T.

    
  * This case does not apply, since the output is wrong.

The proof for the rest of the cases is similar to the proof for the cases 1 to 6, except we replace type equality constraints with equality constraints, type substitution with substitution, and wrong with false.



Suppose C is a set of equality constraints in normal form. Then, C can be interpreted as a substitution θ, and θ is a unifier of all constraints in C. Same can be said for a set of type equality constraints in normal form T.



If C is in normal form, then C = {X_1 = t_1,…, X_n = t_n}, where X_I is a variable and none of X_i occurs in any t_i. So, when we interpret C as a substitution θ, we will have θ = [X_1 ↦ t_1,…,X_n ↦ t_n]. When we apply θ to each constraint in C, we will get θ(C) = {θ(X_1) = θ(t_1), …, θ(X_n) = θ(t_n)}, but since none of the variables X_i occur in any t_i, then θ(t_i) = t_i. Moreover, θ(X_i) = t_i. So we get θ(C) = { t_1 = t_1, … t_n = t_n}. Therefore, θ is a unifier of all constraints in C. The proof for type equality constraints is similar to this one, replacing substitutions with type substitutions and terms with type terms.


We are now ready to prove the following theorem that proves the algorithm outputs a semantically correct value.


Let t_1 and t_2 be the input to the typed unification algorithm, and Γ⊢ t_1 = t_2  | C | T. Suppose (C,T) →^* R.


  * If R = (θ,μ), a pair of substitutions for terms and types respectively, then θ, μ C,T.


  * If R = false, then there is no substitution θ such that θ C, but there is a type substitution μ such that μ T.


  * If R = wrong, then there is no type substitution μ such that μ T.




The proof for (1) follows from Lemmas <ref> and <ref>. We get that θ and μ are unifiers of C and T, respectively.

The proof for (2) follows from the fact that the Martelli-Montanari algorithm is complete, i.e., if there was a unifier for the equality constraint set C, then it would have been obtained. Therefore there is no unifier for C, so there is no θ such that θ C. However, since we got to the second part of the algorithm, then we were able to find a unifier for the type equality constraints. This means that there is at least one unifier for T, so there is a μ such that μ T.

The proof for (3) follows form the fact that the Martelli-Montanari algorithm is complete, i.e., if there was a unifier for the type equality constraint set T, then it would have been obtained. Therefore there is no unifier for T, so there is no μ such that μ T.


Additionally, we want to prove that we always get the principal typing for a term using the constraint generation and solving.


Let t be term, or a unification of two terms, Γ be a generic context, and Δ be type declarations for constants and function symbols. If Γ, Δ⊢ t : τ | C | T and (C,T) →^* (θ,μ). Then (μ(Γ),μ(τ)) is a principal typing of t.



We will prove by structural induction on t.

    
  * If t is a variable X, then (X : α) ∈Γ. We know that Γ, Δ⊢ X : α | ∅ | ∅ by a single application of GVAR. (∅,∅) → ([ ],[ ]), where [ ] are each the identity substitution for variables and type variables, respectively. Therefore [ ](α) = α, and any type τ derived in the type system such that (X:τ) ∈Γ', then τ is an instance of α.

    
  * If t is a constant k, then (k : ∀α⃗. τ) ∈Δ. We know that Γ, Δ⊢ k : τ[α⃗↦σ⃗], for any σ⃗. We get by a single application of rule GCST that Γ, Δ⊢ k : τ[α⃗↦β⃗] | ∅ | ∅. (∅,∅) → ([ ],[ ]), where [ ] are each the identity substitution for variables and type variables, respectively. Therefore [ ](τ[α⃗↦β⃗]) = τ[α⃗↦β⃗], and we known that any σ⃗ is an instance of β⃗.

    
  * If t is a complex term f(t_1,…,t_n), then (f : ∀α⃗. τ_1 ×…×τ_n →τ') ∈Δ. By the induction hypothesis, we know that if (∅,T_i) →^* ([ ],μ_i), then (μ_i(Γ),μ_i(τ'_i)) is a principal typing of t_i. Now suppose (∅,T_1∪…∪ T_n ∪{τ'_1 ≐τ_1[α⃗↦β⃗], …, τ'_n ≐τ_n[α⃗↦β⃗] }) →^* ([ ],μ). We know that μ(τ'_i) = μ(τ_i[α⃗↦β⃗]) for all i = 1,…,n. So we can derive μ(Γ),Δ⊢ t_i : μ(τ_i[α⃗ mapsto β⃗]), and by a single application of rule CPL, we get μ(Γ),Δ⊢ f(t_1,…,t_n) : μ(τ[α⃗↦β⃗]. Now we need to prove that this typing (μ(Γ),μ(τ[α⃗↦β⃗])) is the principal typing. Suppose we had another typing that was not an instance of this one (μ'(Γ),μ'(τ[α⃗↦β⃗])). Since μ is an MGU of T_1∪…∪ T_n ∪{τ'_1 ≐τ_1[α⃗↦β⃗], …, τ'_n ≐τ_n[α⃗↦β⃗] }, then either for some i μ'⊭ T_i, or for some i μ'⊭τ'_i ≐τ_i[α⃗↦β⃗]. If the former is true, then (μ'(Γ),μ('(τ'_i))) is not an instance of the principal typing for t_i and therefore cannot be derived in the type system. If the latter is true, then μ'(τ_i[α⃗↦β⃗]) ≠μ'(τ'_i) and we cannot use the rule CPL in the type system. Therefore, (μ(Γ),μ(τ[α⃗↦β⃗])) is the principal typing for f(t_1,…,t_n).

    
  * Suppose t is an equality t_1 = t_2. By the induction hypothesis, we know that if (∅,T_i) →^* ([ ],μ_i), then (μ_i(Γ),μ_i(τ_i)) is a principal typing of t_i. Now suppose ({t_1 = t_2},T_1∪ T_2∪{τ_1 ≐τ_2) →^* (θ,μ). We know that μ(τ_i) is an instance of μ_i(τ_i), so we can derive μ(Γ),Δ⊢ t_i : μ(τ_i) in the type system. By a single application of rule EQU, we get μ(Γ),Δ⊢ t_1 = t_2 : bool. So (μ(Γ),μ(bool)) is a typing. Suppose it was not the principal typing. Suppose we had another typing that was not an instance of this one (μ'(Γ),μ'(bool)). For all μ, μ(bool) = bool. Since μ is an MGU of T_1 ∪ T_2 ∪{τ_1 ≐τ_2}, then if μ' is not an instance either for some i μ'⊭ T_i or μ⊭τ_1 ≐τ_2. If the former is true, then (μ'(Γ),μ'(τ_1)) is not an instance of its principal typing, so it cannot be derived in the type system. If the latter is true, the types for t_1 and t_2 are different and we cannot apply rule EQU, so we could not have this derivation in the type system. Therefore, (μ(Γ),μ(bool)) is the principal typing for t_1 = t_2.





§ USING REGULAR TYPED UNIFICATION IN PRACTICE
 
Our regular typed unification provides some foundation for the use of regular types to dynamically catch erroneous Prolog behaviors. Indeed, one of the original motivations for this work was to understand how to extend the YAP Prolog system <cit.> with an effective dynamic typing.
Here we will see that, due to efficiency matters, this extension is not able to replace first order unification by regular typed unification in the Prolog engine.

In <cit.> we proposed a typed SLD-resolution (TSLD) which used our previous notion of typed unification. Our goal now is to effectively extend SLD resolution with unification of terms typed by regular types.

A TSLD-tree branch may result in true, false, or wrong, depending on the same results for the unifications in the branch. In <cit.>, each TSLD-tree branch that eventually outputs false, needed to continue execution on the same branch in order to check if there was a type error in some other atom in the query.
This lead to a drastic increase in the runtime of programs.


Consider the following (unrealistic) but possible program:

and query: .
In Prolog SLD-resolution, the first atom in the query fails to unify with the only clause in the program for predicate p, which immediately fails. So there is a single SLD-step.

In the TSLD-resolution defined in <cit.>, since the first 3000 queries return false, we need to reach step 3001 in order to obtain the value wrong.
Note that if the query was  we would only take a single step less, but get the same result as SLD-resolution. 


Pragmatically, it is quite impractical to increase the runtime of programs like this in these cases. This reduction on efficiency would make Prolog an unusable programming language for real applications.

Thus, when adding regular typed unification to Prolog we have a compromise between completeness and efficiency. 

If the evaluation of a query is false we stop execution, and the same happens for wrong. However, if the result is false and there are other atoms in the query, we cannot assure that the value for that branch is indeed false, only that it is not true. Thus, in our extension to Prolog we output no(?) in these cases. On the other hand, we output no(false) if there are no other atoms in the query, and  no(wrong) if the branch ends on wrong.


Consider the same program as above and the query .
After a single TSLD-step we get false, but there is another atom in the query, so Prolog now outputs no(?).

If the query, however, is  we would output no(wrong).


One can ask what would be the point then, to sometimes detect type errors but other times fail to detect them. Well, in many programs, for some queries, we are always able to detect the type error.


Consider the predicate that calculates the length of a list:

One typical bug in Prolog, is to swap the arguments of a predicate.
Now note that, in this case, if we have the erroneous query , both branches of the TSLD-tree output wrong since there is a type error in the first argument (and also in the second).






§ CONCLUSION AND FUTURE WORK

In this paper we present a new unification algorithm for typed terms where types are a subset of regular types which correspond exactly to the usual notion of abstract data types. The work presented here inspires the following possible tasks: 1) Investigate the extension of regular typed unification to other forms of unification. In particular, investigate the extensions to higher-order unification and constraint solving in specific constraint domains. 2) Develop a meta-theory of regular typed unification. In particular, investigate conditions under which unification of terms typed by extensions of regular types, such as closed types or dependent types, satisfies the most general and principal types property and is decidable. 3) Investigate the complexity of regular typed unification. Separately, also investigate the complexity of the set of programs that we are able to type by restrictions of regular types.
Acknowledgements This work was partially financially supported by UIDB/00027/2020 of the Artificial Intelligence and Computer Science Laboratory, LIACC, funded by national funds through the FCT/MCTES (PIDDAC).




