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 query program with, the query program containing one or more queries to a database that contains relations described by at least one a database schema, wherein the database schema specifies a column type for every column of every extensional predicate that occurs in the query program; 
 receiving the database schema and at least one an entity type hierarchy for the database; and 
 inferring a first type program from definitions in the query program by replacing each use of a database relation an extensional predicate in the query program by its type in the conjunction of the column types of the columns of the extensional predicate, the column types being provided by the database schema, and the wherein each column type is at least portion of a respective 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 programs use only extensionals that are monadic extensions, and the first type program and the second type programs do not contain negation; 
 testing portion portions of the first type program that has been inferred for type emptiness and type inclusion; and 
 finding type emptiness or type inclusion for a first portion of the first type program, wherein the first portion is also a type program; and 
 providing at least one of error information and or optimization information regarding the type emptiness and or type inclusion being found for the type first portion of the first type program. 
 
     
     
       2. The computer-implemented method of  claim 1 , further comprising:
 in response to type emptiness being found for a the first portion of the first type program that has been inferred during determining of the testing portion of portions of the first type program, performing at least one of:
 removing the a type test from the query program a first portion of the query program that corresponds to the first portion of the first type program; 
 providing a notification regarding the emptiness found for the first portion of the first type program; or 
 providing notification on combining queries in the query program 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 second portion of the first type program that has been inferred during determining of the testing portion of portions of the first type program, performing at least one of:
 removing the a type test from the query program a second portion of the query program that corresponds to the second portion of the first type program; and or 
 providing a notification regarding the type inclusion being found for the second portion of the first type program. 
 
 
     
     
       4. The computer-implemented method of  claim 1 , further comprising wherein:
 inferring the first type program includes inferring an inferred type for an intensional predicate in the query program that has a declared type in the query program; and 
 the method further comprises: 
 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 
 determining that the inferred type does not contain the declared type; and 
 providing a notification regarding that the database query declared type is not being contained in the given portion inferred type. 
 
     
     
       5. The computer-implemented method of  claim 1 , wherein portions of the first type program that has been inferred are represented by a set respective sets of type tuple constraints (TTCs), wherein each of the TTCs includes:
 a tuple of type propositions; 
 an equivalence relation between tuple components, each tuple component being a type proposition; and 
 a set of inhabitation constraints. 
 
     
     
       6. The computer-implemented method of  claim 5 , further comprising:
 checking inclusion of a third portion of the first type program that has been inferred represented by a first set of TTCs into another, fourth portion of the first 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 determining whether a larger TTC exists in the set of prime implicants of the second set of TTCs; and
 determining that the third portion is included in the fourth portion if for each TTC in the first set a larger TTC exists 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 each of the consensus operations are performed by includes generating a new TTC from two existing TTCs by 
 receiving two TTCs as operands two TTCs, the tuple of type propositions of each TTC having the same number of type propositions; 
 receiving a set of indices and, each index in the set identifying a type proposition in a tuple of type propositions by the position of the type proposition in the tuple;  
 equating in each operand TTC all columns whose indices type propositions at index positions that occur in the set of indices, and preserving all other equalities and inhabitation constraints of the operands each TTC operand, and then for each index position taking disjunctions over columns type propositions indexed in the set of indices and conjunctions over all other columns type propositions as the type propositions of the tuple of type propositions of the new TTC; and 
 takinggenerating a union of two or more of the equivalence relations in of the operands operand TTCs as the equivalence relation between tuple components of the new TTC; and 
 generating a pointwise disjunction of the inhabitation constraints of the operandsoperand TTCs as the inhabitation constraints of the new TTC. 
 
     
     
       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, wherein a TTC τ is covered by a TTC τ′ if τ<:τ′. 
 
     
     
       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 BDD), and choosing a BDD variable order by assigning neighboring indices of the set of 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 further comprising:
 using the first type program as an approximation is used to find erroneous parts of a database query in the query program 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 in the query program 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 the method further comprises:
 using the first type program as an approximation is used to optimize these called the query procedures, by and eliminating query parts from the query procedures 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 comprising:
 computing the context of each query procedure called by a query program by
 traversing a call graph of that query program, and 
 keeping a stack of approximations of all contexts where the query 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 further comprising:
 using the first type program as an approximation is used to optimize queries, in the query program by eliminating from the query program query parts that test whether a value is included in a portion of the first type program  has a particular declared type in the query program, and the approximation first type program indicates at least one of:
 the value will be included in this portion of the first type program have the particular declared type regardless of contents stored in the database; and 
 the value will not be included in the portion of the first type program have the particular declared type regardless of contents stored in the database. 
 
 
     
     
       16. 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 communicatively coupled to the memory and the processor computer program loaded in the computer system, wherein the type inferencer is adapted to cause the computer system perform the operations of:
 accessing a query program with, the query program containing one or more query operations to a database that contains relations described by at least one a database schema, wherein the database schema specifies a column type for every column of every extensional predicate that occurs in the query program; 
 receiving the database schema and at least one an entity type hierarchy for the database; and 
 inferring a first type program from definitions in the query program by replacing each use of a database relation an extensional predicate in the query program by its type in  the conjunction of the column types of the columns of the extensional predicate, the column types being provided by the database schema, and the wherein each column type is at least portion of a respective 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 programs use only extensionals that are monadic extensions, and the first type program and the second type programs do not contain negation; 
 testing portion portions of the first type program that has been inferred for type emptiness and type inclusion; and 
 finding type emptiness or type inclusion for a first portion of the first type program, wherein the first portion is also a type program; and 
 providing at least one of error information and optimization information regarding the type emptiness and or type inclusion being found for the type first portion of the first type program. 
 
 
     
     
       17. The system of  claim 16 , wherein the type inferencer is further adapted to perform the operations of:
 in response to type emptiness being found for a the first portion of the first type program that has been inferred during determining of the testing portion of portions of the first type program, performing at least one of:
 removing a type test  from the query program a first portion of the query program that corresponds to the first portion of the first type program; 
 providing a notification regarding the emptiness found for the first portion of the first type program; or 
 providing notification on combining queries in the query program 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 perform the operations of:
 in response to type inclusion being found for a second portion of the first type program that has been inferred during determining of the testing portion of portions of the first type program, performing at least one of:
 removing a type test  from the query program a second portion of the query program that corresponds to the second portion of the first type program; and or 
 providing a notification regarding the type inclusion being found for the second portion of the first type program. 
 
 
     
     
       19. A non-transitory computer program product, the computer program product comprising instructions for  to cause a computer system to perform the operations of:
 accessing a query program with, the query program containing one or more query operations to a database that contains relations described by at least one a database schema, wherein the database schema specifies a column type for every column of every extensional predicate that occurs in the query program; 
 receiving the database schema and at least one an entity type hierarchy for the database; and 
 inferring a first type program from definitions in the query program by replacing each use of a database relation an extensional predicate in the query program by its type in  the conjunction of the column types of the columns of the extensional predicate, the column types being provided by the database schema, and the wherein each column type is at least portion of a respective 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 programs use only extensionals that are monadic extensions, and the first type program and the second type programs do not contain negation; 
 testing portion portions of the first type program that has been inferred for type emptiness and type inclusion; and 
 finding type emptiness or type inclusion for a first portion of the first type program, wherein the first portion is also a type program; and 
 providing at least one of error information and optimization information regarding the type emptiness and or type inclusion being found for the type first portion of the first type program. 
 
     
     
       20. The non-transitory computer program product of  claim 19 , further comprising instructions to cause the computer system to perform the operations of:
 in response to type emptiness being found for a the first portion of the first type program that has been inferred during determining of the testing portion of portions of the first type program, performing at least one of:
 removing a type test  from the query program a first portion of the query program that corresponds to the first portion of the first type program; 
 providing a notification regarding the emptiness found for the first portion of the first type program; or 
 providing notification on combining queries in the query program 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. The computer-implemented method of claim 1, wherein:
 each of the column types is a monadic type found in a set of type symbols.   
     
     
       22. The computer-implemented method of claim 2, further comprising:
 in response to finding that the first portion of the query program is a conjunction, finding a smallest set of query parts in the first portion of the query program that has a conjunction that is empty, and providing a notification regarding the emptiness found for the smallest set of query parts that has a conjunction that is empty.