Type inference for datalog with complex type hierarchies

Abstract

What is disclosed are a novel system and method for inferring types of database queries. In one embodiment a program and associated database schema that includes a type hierarchy is accessed. The program includes query operations to a database that contains relations described by a database schema. Types are inferred from definitions in the program by replacing each database relationship in the program by the types in the database schema. A new program is generated with the types that have been inferred with the new program only accessing unary relations in the database. In another embodiment, testing of each of the types that have been inferred is performed for type emptiness. In response to type emptiness being found for a type that have been inferred, a variety of different operations are performing including removing the type, providing a notification regarding the emptiness found for the type, and more.

What is claimed is: 
     
       1. A computer-implemented method comprising:
 accessing a program with one or more queries to a database that contains relations described by at least one database schema;   receiving the database schema and at least one entity type hierarchy for the database; and   inferring a first type program from definitions in the program by replacing each use of a database relation in the program by its type in the database schema, and the type is at least portion of a second type program,   wherein each of the first type program and the second type program is a derived program using type symbols without other extensional relation symbols, and each of the first type program and the second type program do not contain negation,   wherein the first type program and the second type program uses monadic extensions;   testing portion of the first type program that has been inferred for type emptiness and type inclusion; and   providing at least one of error information and optimization information regarding the type emptiness and type inclusion being found for the type.   
     
     
       2. The computer-implemented method of  claim 1 , further comprising:
 in response to type emptiness being found for a portion of the first type program that has been inferred during determining of the testing portion of the first type program, performing at least one of:
 removing the a type test; 
 providing a notification regarding the emptiness found for the portion of the first type program; 
 providing notification on combining queries by conjunction without creating empty parts in a combined query; 
   in response to an empty part of a query being a conjunction, finding a smallest set of query parts that has a conjunction that is empty;   in response to a search for a smallest empty part of a database query that traverses all parts of the database query, pushing a conjunction of an approximation of the smallest empty part and a context on top of a stack of approximations of all contexts where the empty part is being used; and   eliminating empty query parts to achieve virtual method resolution in an object-oriented query language.   
     
     
       3. The computer-implemented method of  claim 1 , further comprising:
 in response to type inclusion being found for a portion of the first type program that has been inferred during determining of the testing portion of the first type program, performing at least one of:
 removing the a type test; and 
 providing a notification regarding the type inclusion being found for the portion type. 
   
     
     
       4. The computer-implemented method of  claim 1 , further comprising:
 testing the type program that has been inferred for whether a database query is contained in a given portion of the type program; and in response to the database query not being contained in the given portion, performing at least one of:   removing a type test; and   providing a notification regarding the database query not being contained in the given portion.   
     
     
       5. The computer-implemented method of  claim 1 , wherein portions of the type program that has been inferred are represented by a set of type tuple constraints (TTCs), wherein each of the TTCs includes:
 a tuple of type propositions;   an equivalence relation between tuple components; and   a set of inhabitation constraints.   
     
     
       6. The computer-implemented method of  claim 5 , further comprising:
 checking inclusion of a portion of the type program that has been inferred represented by a first set of TTCs into another portion of the type program represented by a second set of TTCs by computing a set of prime implicants of the second set; and   checking each TTC in the first set and finding a larger TTC in the set of prime implicants of the second set of TTCs.   
     
     
       7. The computer-implemented method of  claim 6 , further comprising:
 computing the set of prime implicants of the second set of TTCs by saturating the second set by exhaustively applying consensus operations to ensure all relevant TTCs are included.   
     
     
       8. The computer-implemented method of  claim 7 , wherein the consensus operations are performed by
 receiving two TTCs as operands;   receiving a set of indices and equating all columns whose indices occur in the set, and preserving all other equalities and inhabitation constraints of the operands, and taking disjunctions over columns in the set and conjunctions over all other columns; and   taking a union of two or more of the equivalence relations in the operands and a pointwise disjunction of the inhabitation constraints of the operands.   
     
     
       9. The computer-implemented method of  claim 8 , further comprising:
 reducing a number of consensus operations that need to be performed during saturation by omitting consensus operations where a resulting TTC will be covered by TTCs already present in the set.   
     
     
       10. The computer-implemented method of  claim 8 , further comprising:
 receiving a logical formula that represents a type hierarchy, and representing a component type proposition of a TTC as a binary decision diagram (BDDs), and choosing a BDD variable order by assigning neighboring indices to type symbols that appear in a same conjunct of the logical formula that represents the type hierarchy.   
     
     
       11. The computer-implemented method of  claim 1 , wherein an approximation is used to find erroneous parts of a database query that will return an empty set of results, regardless of contents stored in the database. 
     
     
       12. The computer-implemented method of  claim 2 , wherein the providing notification on combining queries by conjunction without creating empty parts in a combined query includes depicting compatible types with similar pictures in a user interface. 
     
     
       13. The computer-implemented method of  claim 1 , wherein the one or more queries to the database contain calls to other query procedures, and an approximation is used to optimize these called procedures, by eliminating query parts that will return an empty set of results in a context where they are called, regardless of any contents of the database. 
     
     
       14. The computer-implemented method of  claim 13 , wherein the context of a procedure in a database query is computed by
 traversing a call graph of that query, and   keeping a stack of approximations of all contexts where the procedure is being used, and   when entering a procedure in the call graph, pushing a conjunction of an approximation of a body of that procedure and a top of the stack onto the stack as a new context.   
     
     
       15. The computer-implemented method of  claim 1 , wherein an approximation is used to optimize queries, by eliminating query parts that test whether a value is included in a portion of the first type program, and the approximation indicates at least one of:
 the value will be included in this portion of the first type program regardless of contents stored in the database; and   the value will not be included in the portion of the first type program.   
     
     
       16. A system comprising:
 a memory;   a processor communicatively coupled to the memory; and   a type inferencer communicatively coupled to the memory and the processor, wherein the type inferencer is adapted to:   accessing a program with one or more query operations to a database that contains relations described by at least one database schema;   receiving the database schema and at least one entity type hierarchy for the database; and   inferring a first type program from definitions in the program by replacing each use of a database relation in the program by its type in the database schema, and the type is at least portion of a second type program,   wherein each of the first type program and the second type program is a derived program using type symbols without other extensional relation symbols, and each of the first type program and the second type program do not contain negation,   wherein the first type program and the second type program uses monadic extensions;   testing portion of the first type program that has been inferred for type emptiness and type inclusion; and   providing at least one of error information and optimization information regarding the type emptiness and type inclusion being found for the type.   
     
     
       17. The system of  claim 16 , wherein the type inferencer is further adapted to:
 in response to type emptiness being found for a portion of the first type program that has been inferred during determining of the testing portion of the first type program, performing at least one of:
 removing a type test; 
 providing a notification regarding the emptiness found for the portion of the first type program; 
 providing notification on combining queries by conjunction without creating empty parts in a combined query; 
   in response to an empty part of a query being a conjunction, finding a smallest set of query parts that has a conjunction that is empty;   in response to a search for a smallest empty part of a database query that traverses all parts of the database query, pushing a conjunction of an approximation of the smallest empty part and a context on top of a stack of approximations of all contexts where the empty part is being used; and   eliminating empty query parts to achieve virtual method resolution in an object-oriented query language.   
     
     
       18. The system of  claim 16 , wherein the type inferencer is further adapted to:
 in response to type inclusion being found for a portion of the first type program that has been inferred during determining of the testing portion of the first type program, performing at least one of:   removing a type test; and   providing a notification regarding the type inclusion being found for the portion type.   
     
     
       19. A non-transitory computer program product, the computer program product comprising instructions for:
 accessing a program with one or more query operations to a database that contains relations described by at least one database schema;   receiving the database schema and at least one entity type hierarchy for the database; and   inferring a first type program from definitions in the program by replacing each use of a database relation in the program by its type in the database schema, and the type is at least portion of a second type program,   wherein each of the first type program and the second type program is a derived program using type symbols without other extensional relation symbols, and each of the first type program and the second type program do not contain negation,   wherein the first type program and the second type program uses monadic extensions;   testing portion of the first type program that has been inferred for type emptiness and type inclusion; and   providing at least one of error information and optimization information regarding the type emptiness and type inclusion being found for the type.   
     
     
       20. The non-transitory computer program product of  claim 19 , further comprising:
 in response to type emptiness being found for a portion of the first type program that has been inferred during determining of the testing portion of the first type program, performing at least one of:
 removing a type test; 
 providing a notification regarding the emptiness found for the portion of the first type program; 
 providing notification on combining queries by conjunction without creating empty parts in a combined query; 
   in response to an empty part of a query being a conjunction, finding a smallest set of query parts that has a conjunction that is itself empty;   in response to a search for a smallest empty part of a database query that traverses all parts of the database query, pushing a conjunction of an approximation of that part and a context on top of a stack; and   eliminating empty query parts to achieve virtual method resolution in an object-oriented query language.   
     
     
       21. A computer program product, the computer program product comprising a hardware storage device comprising instructions to cause a computer system to perform operations comprising:
 obtaining a query program that queries a database described by a database schema that specifies a column type for every column of every extensional predicate that occurs in the query program and also described by a type hierarchy that is of the form ∀x.h(x) in which h(x) does not contain quantifiers or equations and only contains a single free variable x;   representing the query program by a first type program having no free relation variables and having no fixpoint definitions containing intensional relation variables, wherein the column type is at least a portion of a second type program, wherein each of the first type program and the second type program is a derived program, and wherein each of the first type program and the second type program uses monadic extensionals, a type program being a program that only makes use of type symbols and no other extensional relation symbols and that only has instances of negation in front of type symbols that are the names of monadic extensionals;   translating the first type program into a typing, wherein the typing is a lean set of non-degenerate n-ary type tuple constraints (TTCs), each TTC being defined by   (i) a tuple (t1, . . . tn) of n type propositions ti, a type proposition being a quantifier-free type program with no fixpoint definitions and no free relation variables and having precisely one free element variable,   (ii) an equivalence relation over the set of integers {1, . . . , n} that defines a partition of the set of integers {1, . . . , n}; and   (iii) a set C of inhabitation constraints, each inhabitation constraint being a type proposition, the inhabitation constraints modeling existential quantification;   such that the following three requirements are satisfied whenever i and j belong to the same partition under the equivalence relation:
   t i =t j , 
   C<:t k  for all k∈{1, . . . , n}, and   c<:c′ for c, c′∈C implies c=c′;   testing a first TTC of the typing for type emptiness and type inclusion; and   providing at least one of error information and optimization information regarding the type emptiness and type inclusion being found for a type program represented by the TTC.   
     
     
       22. The computer program product of claim 21, wherein:
 the type propositions of the TTCs do not contain negation.   
     
     
       23. The computer program product of claim 21, wherein:
 the type hierarchy includes one or more of (i) a statement of implication between entity types, (ii) a statement of equivalence of entity types, or (iii) a statement of disjointness of entity types.   
     
     
       24. The computer program product of claim 21, wherein:
 translating the first type program into the typing comprises eliminating all non-maximal and degenerate TTCs from the set of TTCs.   
     
     
       25. The computer program product of claim 21, further comprising instructions to cause the computer system to perform the operations of:
 representing the TTCs in the typing by encoding the component type propositions of the TTCs as binary decision diagrams.   
     
     
       26. The computer program product of claim 21, further comprising instructions to cause the computer system to perform the operations of:
 building a TTC∥τ∥ from a pre-TTC, the pre-TTC being a structure τ=(t 1 , . . . , t n |p|C), in which t 1 , . . . , t n  are a tuple of type propositions, p is a relation over {1, . . . , n}, C is a set of inhabitation constraints, which are type propositions, and τ does not satisfy at least one of the three requirements, by setting:
   ∥τ∥:=(∥t 1 ∥   p   , . . . ,∥t n ∥   p   | p |min(C∪{t 1 , . . . ,t n }))
 
   
       where
 ∥t i ∥ q =∧{t j |i˜ q j}, where i˜ q j states that i and j belong to the same partition in q, and 
   p  is a smallest equivalence relation containing the relation p. 
 
     
     
       27. The computer program product of claim 21, wherein the query program is a first query program and the typing is a first typing, the operations further comprising:
 obtaining a second query program that queries a second database that is described by the database schema and the type hierarchy;   representing the second query program by a third type program having no free relation variables and having no fixpoint definitions containing intensional relation variables;   translating the third type program into a second typing; and   performing a containment check on the first typing and the second typing to determine whether the first type program contains the third type program.   
     
     
       28. The computer program product of claim 27, wherein the data in the second database is different from the data in the first database. 
     
     
       29. The computer program product of claim 21, further comprising:
 performing type specialization and type erasure using the typing to optimize the query program.   
     
     
       30. The computer program product of claim 21, wherein the first type program is without fixpoint definitions and has intentional relation variables r 1 , . . . , r m  and element variables x 1 , . . . , x n , and wherein translating the first type program into a typing comprises performing recursion on the structure of the first type program to translate the first type program, denoted φ, to a mapping (φ): Typing m →Typing, the mapping being a mapping from a tuple of m typings {right arrow over (T)}, wherein each of the m typings is associated with a respective one of the m relation variables r 1 , . . . , r m  and the recursion is defined by:
     ⊥ ({right arrow over (T)})=∅
 
     x i ≐x j   ({right arrow over (T)})={(T, . . . , T| {[i,j]} )}
 
     u(x j ) ({right arrow over (T)})={T TTC   j:=u } 
     ¬u(x j ) ({right arrow over (T)})={T TTC   j:=¬u }
 
     r i ({right arrow over (x)}) ({right arrow over (T)})=T i    
     ψ∧χ ({right arrow over (T)})= ψ ({right arrow over (T)}) ∧   χ ({right arrow over (T)})
 
     ψ∨χ ({right arrow over (T)})= ψ ({right arrow over (T)}) ∨   χ ({right arrow over (T)})
 
     ∃ x     i   .ψ ({right arrow over (T)})=∃ i ( ψ ({right arrow over (T)}))
 
 wherein
 the i-th existential of a TTC τ=(t 1 , . . . , t n |p|C) is defined as ∃ i (τ):=(t 1 , . . . , t i-1 , t i+1 , . . . , t n |p′|min(C∪{t i })) 
 
 where p′ is the restriction of p to {1,. . . ,i−1,i+1, . . . ,n} and
 the i-th existential of a typing T is defined pointwise as ∃ i (T) := max ⊥  {∃ i (τ)|τ∈T}, 
 
 where the operation max ⊥  on a set of TTCs removes all non-maximal and degenerate TTCs from the set of TTCs;
 binary meets and joins of two typings T and T′ are defined pointwise and respectively as T ∧ T′=max ⊥ ({τ ∧ τ′|τ∈T,τ′∈T′}) and T ∨ T′=max ⊥ (T∪T′); 
 
 {T TTC } is a greatest element under the order <: on a typing, and {T TTC   j:=u } is a second TTC resulting from a first TTC {T TTC } by replacing the j-th type proposition in the tuple of type propositions of the first TTC by u in the second TTC and adding u to the inhabitation constraints of the second TTC; and 
 {(T, . . . , T| [{i,j}] )} denotes a set of TTCs, which is a typing, with a single TTC in the set, which single TTC has every component of its tuple of type propositions is equal to T, which single TTC has as its partition the smallest equivalence relation in which i and j are equivalent, and which single TTC is trivial; 
 wherein the overall typing is the least fixpoint of the resulting typings {right arrow over (T)} after the recursion is complete. 
 
     
     
       31. A system comprising:
 a computer system comprising one or more computers each having a memory and a processor communicatively coupled to the memory; and   a type inferencer computer program loaded in the computer system, wherein the type inferencer is adapted to cause the computer system to perform the operations of:   obtaining a query program that queries a database described by a database schema that specifies a column type for every column of every extensional predicate that occurs in the query program and also described by a type hierarchy that is of the form ∀x.h(x) in which h(x) does not contain quantifiers or equations and only contains a single free variable x;   representing the query program by a first type program having no free relation variables and having no fixpoint definitions containing intensional relation variables, wherein the column type is at least a portion of a second type program, wherein each of the first type program and the second type program is a derived program, and wherein each of the first type program and the second type program uses monadic extensionals, a type program being a program that only makes use of type symbols and no other extensional relation symbols and that only has instances of negation in front of type symbols that are the names of monadic extensionals;   translating the first type program into a typing, wherein the typing is a lean set of non-degenerate n-ary type tuple constraints (TTCs), each TTC being defined by   (i) a tuple (t1, . . . tn) of n type propositions ti, a type proposition being a quantifier-free type program with no fixpoint definitions and no free relation variables and having precisely one free element variable,   (ii) an equivalence relation over the set of integers {1, . . . , n} that defines a partition of the set of integers {1, . . . , n}, and   (iii) a set C of inhabitation constraints, each inhabitation constraint being a type proposition, the inhabitation constraints modeling existential quantification;   such that the following three requirements are satisfied whenever i and j belong to the same partition under the equivalence relation:   t i =t j ,   C<:t k  for all k∈{1, . . . , n}, and   c<:c′ for c, c′∈C implies c=c′;   testing a first TTC of the typing for type emptiness and type inclusion; and   providing at least one of error information and optimization information regarding the type emptiness and type inclusion being found for a type program represented by the TTC.   
     
     
       32. The system of claim 31, wherein:
 the type propositions of the TTCs do not contain negation.   
     
     
       33. The system of claim 31, wherein:
 the type hierarchy includes one or more of (i) a statement of implication between entity types, (ii) a statement of equivalence of entity types, or (iii) a statement of disjointness of entity types.   
     
     
       34. The system of claim 31, wherein:
 translating the first type program into the typing comprises eliminating all non-maximal and degenerate TTCs from the set of TTCs.   
     
     
       35. The system of claim 31, the operations further comprising:
 representing the TTCs in the typing by encoding the component type propositions of the TTCs as binary decision diagrams.   
     
     
       36. The system of claim 31, the operations further comprising:
 building a TTC ∥τ∥ from a pre-TTC, the pre-TTC being a structure τ=(t 1 , . . . , t n |p|C), in which t 1 , . . . , t n  are a tuple of type propositions, p is a relation over {1, . . . , n}, C is a set of inhabitation constraints, which are type propositions, and τ does not satisfy at least one of the three requirements, by setting:
   ∥τ∥:=(∥t 1 ∥   p   , . . . ,∥t n ∥   p   | p |min(C∪{t 1 , . . . , t n }))
 
   
       where
 ∥t i ∥ q =∧{t j |i˜ q j}, where i˜ q j states that i and j belong to the same partition in q, and  p  is a smallest equivalence relation containing the relation p. 
 
     
     
       37. The system of claim 31, wherein the query program is a first query program and the typing is a first typing, the operations further comprising:
 obtaining a second query program that queries a second database that is described by the database schema and the type hierarchy;   representing the second query program by a third type program having no free relation variables and having no fixpoint definitions containing intensional relation variables;   translating the third type program into a second typing; and   performing a containment check on the first typing and the second typing to determine whether the first type program contains the third type program.   
     
     
       38. The system of claim 37, wherein the data in the second database is different from the data in the first database. 
     
     
       39. The system of claim 31, the operations further comprising:
 performing type specialization and type erasure using the typing to optimize the query program.   
     
     
       40. The system of claim 31, wherein the first type program is without fixpoint definitions and has intentional relation variables r 1 , . . . , r m  and element variables x i , . . . , x n , and wherein translating the first type program into a typing comprises performing recursion on the structure of the first type program to translate the first type program, denoted φ, to a mapping (φ): Typing m →Typing, the mapping being a mapping from a tuple of m typings {right arrow over (T)}, wherein each of the m typings is associated with a respective one of the m relation variables r 1 , . . . , r m  and the recursion is defined by:
     ⊥ ({right arrow over (T)})=∅
 
     x i ≐x j   ({right arrow over (T)})={(T, . . . , T| {[i,j]} )}
 
     u(x j ) ({right arrow over (T)})={T TTC   j:=u } 
     ¬u(x j ) ({right arrow over (T)})={T TTC   j:=¬u }
 
     r i ({right arrow over (x)}) ({right arrow over (T)})=T i    
     ψ∧χ ({right arrow over (T)})= ψ ({right arrow over (T)}) ∧   χ ({right arrow over (T)})
 
     ψ∨χ ({right arrow over (T)})= ψ ({right arrow over (T)}) ∨   χ ({right arrow over (T)})
 
     ∃ x     i   .ψ ({right arrow over (T)})=∃ i ( ψ ({right arrow over (T)}))
 
 wherein
 the i-th existential of a TTC τ=(t 1 , . . . , t n |p|C) is defined as ∃ i (τ):=(t 1 , . . . ,t i-1 ,t 1+1 , . . . ,t n |p′|min(C∪{t i })) 
 
 where p′ is the restriction of p to {1, . . . ,i−1,i+1, . . . , n} and
 the i-th existential of a typing T is defined pointwise as ∃ i (T):=max ⊥ {∃ i (τ)|τ∈T}, 
 
 where the operation max ⊥  on a set of TTCs removes all non-maximal and degenerate TTCs from the set of TTCs;
 binary meets and joins of two typings T and T′ are defined pointwise and respectively as T ∧ T′=max ⊥ ({τ ∧ τ′|τ∈T,τ′∈T′}) and T ∨ T′=max ⊥ (T∪T′); 
 
 {T TTC } is a greatest element under the order <: on a typing, and {T TTC   j=u } is a second TTC resulting from a first TTC {T TTC } by replacing the j-th type proposition in the tuple of type propositions of the first TTC by u in the second TTC and adding u to the inhabitation constraints of the second TTC; and 
 {(T, . . . ,T| {[i,j]} )} denotes a set of TTCs, which is a typing, with a single TTC in the set, which single TTC has every component of its tuple of type propositions is equal to T, which single TTC has as its partition the smallest equivalence relation in which i and j are equivalent, and which single TTC is trivial; 
 wherein the overall typing is the least fixpoint of the resulting typings {right arrow over (T)} after the recursion is completed. 
 
     
     
       41. A computer-implemented method comprising:
 obtaining a query program that queries a database described by a database schema that specifies a column type for every column of every extensional predicate that occurs in the query program and also described by a type hierarchy that is of the form ∀x.h(x) in which h(x) does not contain quantifiers or equations and only contains a single free variable x;   representing the query program by a first type program having no free relation variables and having no fixpoint definitions containing intensional relation variables, wherein the column type is at least a portion of a second type program, wherein each of the first type program and the second type program is a derived program, and wherein each of the first type program and the second type program uses monadic extensionals, a type program being a program that only makes use of type symbols and no other extensional relation symbols and that only has instances of negation in front of type symbols that are the names of monadic extensionals;   translating the first type program into a typing, wherein the typing is a lean set of non-degenerate n-ary type tuple constraints (TTCs), each TTC being defined by   (i) a tuple (t1, . . . tn) of n type propositions ti, a type proposition being a quantifier-free type program with no fixpoint definitions and no free relation variables and having precisely one free element variable,   (ii) an equivalence relation over the set of integers {1, . . . , n} that defines a partition of the set of integers {1, . . . , n}, and   (iii) a set C of inhabitation constraints, each inhabitation constraint being a type proposition, the inhabitation constraints modeling existential quantification;   such that the following three requirements are satisfied whenever i and j belong to the same partition under the equivalence relation:   t i =t j ,   C<:t k  for all k∈{1, . . . , n}, and   c<:c′ for c, c′∈C implies c=c′;   testing a first TTC of the typing for type emptiness and type inclusion; and   providing at least one of error information and optimization information regarding the type emptiness and type inclusion being found for a type program represented by the TTC.   
     
     
       42. The method of claim 41, wherein:
 the type propositions of the TTCs do not contain negation.   
     
     
       43. The method of claim 41, wherein:
 the type hierarchy includes one or more of (i) a statement of implication between entity types, (ii) a statement of equivalence of entity types, or (iii) a statement of disjointness of entity types.   
     
     
       44. The method of claim 41, wherein:
 translating the first type program into the typing comprises eliminating all non-maximal and degenerate TTCs from the set of TTCs.   
     
     
       45. The method of claim 41, further comprising:
 representing the TTCs in the typing by encoding the component type propositions of the TTCs as binary decision diagrams.   
     
     
       46. The method of claim 41, further comprising:
 building a TTC ∥τ∥ from a pre-TTC, the pre-TTC being a structure τ=(t 1 , . . . , t n |p|C), in which t 1 , . . . , t n  are a tuple of type propositions, p is a relation over {1, . . . , n}, C is a set of inhabitation constraints, which are type propositions, and τ does not satisfy at least one of the three requirements, by setting:
   ∥τ∥:=(∥t 1 ∥   p   , . . . ,∥t n ∥   p   | p |min(C∪{t 1 , . . . ,t n }))
 
   
       where
 ∥t i ∥ q =∧{t j |i˜ q j}, where i˜ q j states that i and j belong to the same partition in q, and  p  is a smallest equivalence relation containing the relation p. 
 
     
     
       47. The method of claim 41, wherein the query program is a first query program and the typing is a first typing, the method further comprising:
 obtaining a second query program that queries a second database that is described by the database schema and the type hierarchy;   representing the second query program by a third type program having no free relation variables and having no fixpoint definitions containing intensional relation variables;   translating the third type program into a second typing; and   performing a containment check on the first typing and the second typing to determine whether the first type program contains the third type program.   
     
     
       48. The method of claim 47, wherein the data in the second database is different from the data in the first database. 
     
     
       49. The method of claim 41, further comprising:
 performing type specialization and type erasure using the typing to optimize the query program.   
     
     
       50. The method of claim 41, wherein the first type program is without fixpoint definitions and has intentional relation variables r 1 , . . . , r m  and element variables x 1 , . . . , x n , and wherein translating the first type program into a typing comprises performing recursion on the structure of the first type program to translate the first type program, denoted φ, to a mapping (℠): Typing m →Typing, the mapping being a mapping from a tuple of m typings {right arrow over (T)}, wherein each of the m typings is associated with a respective one of the m relation variables r 1 , . . . , r m  and the recursion is defined by:
     ⊥ ({right arrow over (T)})=∅
 
     x i ≐x j   ({right arrow over (T)})={(T, . . . , T| {[i,j]} )}
 
     u(x j ) ({right arrow over (T)})={T TTC   j:=u } 
     ¬u(x j ) ({right arrow over (T)})={T TTC   j:=¬u }
 
     r i ({right arrow over (x)}) ({right arrow over (T)})=T i    
     ψ∧χ ({right arrow over (T)})= ψ ({right arrow over (T)}) ∧   χ ({right arrow over (T)})
 
     ψ∨χ ({right arrow over (T)})= ψ ({right arrow over (T)}) ∨   χ ({right arrow over (T)})
 
     ∃ x     i   .ψ ({right arrow over (T)})=∃ i ( ψ ({right arrow over (T)}))
 
 wherein
 the i-th existential of a TTC τ=(t 1 , . . . , t n |p|C) is defined as ∃ i (τ):=(t 1 , . . . ,t i-1 ,t 1+1 , . . . ,t n |p′| min(C∪{t i })) 
 
 where p′ is the restriction of p to {1, . . . , i−1, i+1, . . . , n} and
 the i-th existential of a typing T is defined pointwise as ∃ i (T):=max ⊥ {∃ i (τ)|τ∈T}, 
 
 where the operation max ⊥  on a set of TTCs removes all non-maximal and degenerate TTCs from the set of TTCs;
 binary meets and joins of two typings T and T′ are defined pointwise and respectively as T ∧ T′=max ⊥ ({τ ∧ τ′|τ∈T,τ′∈T′}) and T ∨ T′=max ⊥ (T∪T′); 
 
 {T TTC } is a greatest element under the order <: on a typing, and {T TTC   j=u } is a second TTC resulting from a first TTC {T TTC } by replacing the j-th type proposition in the tuple of type propositions of the first TTC by u in the second TTC and adding u to the inhabitation constraints of the second TTC; and 
 {(T, . . . ,T| {[i,j]} )} denotes a set of TTCs, which is a typing, with a single TTC in the set, which single TTC has every component of its tuple of type propositions is equal to T, which single TTC has as its partition the smallest equivalence relation in which i and j are equivalent, and which single TTC is trivial; 
 wherein the overall typing is the least fixpoint of the resulting typings {right arrow over (T)} after the recursion is completed. 
 
     
     
       51. A computer program product, the computer program product comprising a hardware storage device comprising instructions to cause a computer system to perform operations comprising:
 obtaining a query program that queries a database described by a database schema that specifies a column type for every column of every extensional predicate that occurs in the query program and also described by a type hierarchy that is of the form ∀x.h(x) in which h(x) does not contain quantifiers or equations and only contains a single free variable x;   representing the query program by a first type program having no free relation variables and having no fixpoint definitions containing intensional relation variables, wherein the column type is at least a portion of a second type program, wherein each of the first type program and the second type program is a derived program, and wherein each of the first type program and the second type program uses monadic extensionals, a type program being a program that only makes use of type symbols and no other extensional relation symbols, and wherein the first type program and the second type program do not contain negation;   translating the first type program into a typing, wherein the typing is a lean set of non-degenerate n-ary type tuple constraints (TTCs), each TTC being defined by   (i) a tuple (t1, . . . tn) of n type propositions ti, a type proposition being a quantifier-free type program with no fixpoint definitions and no free relation variables and having precisely one free element variable,   (ii) an equivalence relation over the set of integers {1, . . . , n} that defines a partition of the set of integers {1, . . . , n}, and   (iii) a set C of inhabitation constraints, each inhabitation constraint being a type proposition, the inhabitation constraints modeling existential quantification;   such that the following three requirements are satisfied whenever i and j belong to the same partition under the equivalence relation:   t i =t j ,   C<:t k  for all k∈{1, . . . , n}, and   c<:c′ for c, c′∈C implies c=c′;   testing a first TTC of the typing for type emptiness and type inclusion; and   providing at least one of error information and optimization information regarding the type emptiness and type inclusion being found for a type program represented by the TTC.   
     
     
       52. A system comprising:
 a computer system comprising one or more computers each having a memory and a processor communicatively coupled to the memory; and   a type inferencer computer program loaded in the computer system, wherein the type inferencer is adapted to cause the computer system perform the operations of:   obtaining a query program that queries a database described by a database schema that specifies a column type for every column of every extensional predicate that occurs in the query program and also described by a type hierarchy that is of the form ∀x.h(x) in which h(x) does not contain quantifiers or equations and only contains a single free variable x;   representing the query program by a first type program having no free relation variables and having no fixpoint definitions containing intensional relation variables, wherein the column type is at least a portion of a second type program, wherein each of the first type program and the second type program is a derived program, and wherein each of the first type program and the second type program uses monadic extensionals, a type program being a program that only makes use of type symbols and no other extensional relation symbols, and wherein the first type program and the second type program do not contain negation;   translating the first type program into a typing, wherein the typing is a lean set of non-degenerate n-ary type tuple constraints (TTCs), each TTC being defined by   (i) a tuple (t1, . . . tn) of n type propositions ti, a type proposition being a quantifier-free type program with no fixpoint definitions and no free relation variables and having precisely one free element variable,   (ii) an equivalence relation over the set of integers {1, . . . , n} that defines a partition of the set of integers {1, . . . , n}, and   (iii) a set C of inhabitation constraints, each inhabitation constraint being a type proposition, the inhabitation constraints modeling existential quantification;   such that the following three requirements are satisfied whenever i and j belong to the same partition under the equivalence relation:   t i =t j ,   C<:t k  for all k∈{1, . . . , n}, and   c<:c′ for c, c′∈C implies c=c′;   testing a first TTC of the typing for type emptiness and type inclusion; and   providing at least one of error information and optimization information regarding the type emptiness and type inclusion being found for a type program represented by the TTC.   
     
     
       53. A computer-implemented method comprising:
 obtaining a query program that queries a database described by a database schema that specifies a column type for every column of every extensional predicate that occurs in the query program and also described by a type hierarchy that is of the form ∀x.h(x) in which h(x) does not contain quantifiers or equations and only contains a single free variable x;   representing the query program by a first type program having no free relation variables and having no fixpoint definitions containing intensional relation variables, wherein the column type is at least a portion of a second type program, wherein each of the first type program and the second type program is a derived program, and wherein each of the first type program and the second type program uses monadic extensionals, a type program being a program that only makes use of type symbols and no other extensional relation symbols, and wherein the first type program and the second type program do not contain negation;   translating the first type program into a typing, wherein the typing is a lean set of non-degenerate n-ary type tuple constraints (TTCs), each TTC being defined by   (i) a tuple (t1, . . . tn) of n type propositions ti, a type proposition being a quantifier-free type program with no fixpoint definitions and no free relation variables and having precisely one free element variable,   (ii) an equivalence relation over the set of integers {1, . . . , n} that defines a partition of the set of integers {1, . . . , n}, and   (iii) a set C of inhabitation constraints, each inhabitation constraint being a type proposition, the inhabitation constraints modeling existential quantification;   such that the following three requirements are satisfied whenever i and j belong to the same partition under the equivalence relation:   t i =t j ,   C<:t k  for all k∈{1, . . . , n}, and   c<:c′ for c, c′∈C implies c=c′;   testing a first TTC of the typing for type emptiness and type inclusion; and   providing at least one of error information and optimization information regarding the type emptiness and type inclusion being found for a type program represented by the TTC.