Semantic Subtyping with an SMT Solver
- Date and Time
Thursday, December 16th, 2010 at 13:30
Polacksbacken, room 1112
The SQL Server Modelling Language M uses types corresponding to relational schemas, and has expressions that compile to SQL queries. M uses a novel combination of type-test and refinement types. Refinement types are used to express SQL table constraints within a type system, and type-tests are useful for processing relational data, for example, by discriminating dynamically between different forms of union types. Still, although useful and extremely expressive, the combination of type-test and refinement is hard to type-check using conventional syntax-driven subtyping rules. The preliminary implementation of M uses such subtyping rules and has difficulty with certain sound idioms (such as uses of singleton and union types). Hence, type safety is enforced by dynamic checks, or not at all.
We formulate a semantics in which expressions denote terms, and types are interpreted as first-order logic formulas. Subtyping is defined as valid implication between the semantics of types. The formulas are interpreted in a specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on an SMT solver to compute subtyping efficiently. Moreover, using an SMT solver allows us to show the uniqueness of normal forms for non-deterministic expressions, to provide precise counterexamples when type-checking fails, to detect empty types, and to compute instances of types statically and at run-time.