Safe Database Abstractions with Type-Level Record Computation Adam Chlipala RADICAL 2010 In the Wild... Written in a general-purpose programming language Application query(“SELECT Id FROM User WHERE Id = '“ + escape(name) + “'”) SELECT Id FROM User WHERE Name = 'foo' Database 2 Language-Integrated Query SELECT Id FROM User WHERE Name = 'foo' Database Query Compiler Application u <­ User; filter(u.Name = name); return u.Id 3 Language or Library? SELECT Id FROM User WHERE Name = 'foo' Database Query Compiler Query Compiler Application u <­ User; filter(u.Name = name); return u.Id Library? Bridging the gap? Programmers can add support for new query languages, without touching the main compiler. ● Can take full advantage of the target language, by building new libraries as needed. ● Language? How do we know this is done right? Static checking of query syntax ● Static guarantee that every query is compiled properly ● Compile-time optimization removes interpretation overhead. ● 4 First-Class Queries in Ur/Web Ur/Web compiler SQL-specific optimization Ur/Web standard library Syntax and typing of SQL as a module system signature Ur A general-purpose language based on ML, Haskell, and Coq Expressive type system supporting type-level computation with records 5 Safe Abstractions via Types u <­ User; filter(u.Name = name); return u.Id bind [#U] (from [#U] user) (seq (filter (eq Comprehension (field [#U] [#Name]) Library (const name)) (select {Id = field [#U] [#Id]})) SELECT Id FROM User WHERE Name = {name} 6 Optimization for Free bind [#U] (from [#U] user) (seq (filter (eq (field [#U] [#Name]) (const name)) (select {Id = field [#U] [#Id]})) Comprehension Library Database SELECT Id FROM User WHERE Name = $1 3. Optimized code iterates over results (often without any heap allocation) $1 = “foo” SELECT Id 1.FROM Compile prepared User 2. Execute with statement once = {name} WHERE Name parameters Application 7 Type Inference for Free SELECT Id FROM User WHERE Name = {name} Syntax-directed translation select {From = {U = user}, Where = eq (field [#U] [#Name]) (const name), Select = pick {U = subset [[Id = _]]}} Generic type inference engine Fully-annotated program 8 Typing SELECT First class polymorphism with higher kinds Type-level map over records The kind of records of records of types val select : full :: {{Type}} ­> keep :: {{Type}} ­> {From : $(map sql_table full), Where : sql_exp full bool, Select : pick keep full} ­> sql_query keep Lightweight “proofs” Richly-typed abstract syntax 9 SQL Expression Syntax type sql_exp :: {{Type}} ­> Type ­> Type val const : ts :: {{Type}} ­> t :: Type ­> sql t ­> t ­> sql_exp ts t Expression type, according to SQL typing {{Type}} ­> t type-level :: Type First-class, namesrules Typing environment val eq : ts :: ­> sql_exp ts t ­> sql_exp ts t ­> sql_exp ts witness bool Type class Type-level computation with records Record disjointness constraints val field : tn :: Name ­> nm :: Name ­> t :: Type ­> fs :: {Type} ­> ts :: {{Type}} ­> [[tn] ~ ts] => [[nm] ~ fs] => sql_exp ([tn = [nm = t] ++ fs] ++ ts) t 10 Implementing Comprehensions from_table t x1 <­ ....; x2 <­ ....; .... xn <­ ....; return .... x1 1 SELECT * FROM ..., t, ... y1 <­ ....; .... ym <­ ....; return .... t1.A t2.B typex2exp t1.C (env t2.B + 6:: {{Type}}) (t :: Type) = ts :: {{Type}} x1.A + 2 * x2.B ­> ...$(map (fn r => $(map (sql_exp ts) r)) env) ­> sql_exp ts t xn t3.X t3.Y t1.A 11 Supported SQL Features ● Inner and outer joins ● Grouping and aggregation ● Relational operators (union, intersection, ...) ● Subqueries ● Sorting of results (“ORDER BY”) ● Table constraints (foreign keys, ...) ● Views ● Insert/update/delete 12 Checking Security Policies Table X Id Name Public F T F T Table Y Id Usr 42 42 6 Policy:SMT Solver SELECT Id, Name Equality FROM X Functions WHERE PublicDatatypes ● ● “known” ●Functional dependencies ● est u q e TP R Y_id 6 8 8 ● HT Access Control List Web App Policy: SELECT Y.* FROM Y, Acl, User WHERE Y_id = Y.Id AND Usr = User.Id AND known(User.Pass) known = {42, “foo”}* Static Verifier User: 42 Password: foo 13 Ur/Web Available At: http://www.impredicative.com/ur/ Including online demos with syntax-highlighted source code 14 Smart Type Inference fun foo [ts :: {{Type} * Type}] (fl : folder ts) (tabs : $(map (fn (fs, _) => sql_table fs) ts)) (funcs : $(map (fn (fs, t) => $fs ­> t) ts)) : list $(map (fn (_, t) => t) ts) = .... select {From = (* build record from tabs *), ...} The Ur inference .... engine must apply a fusion law! $(map (fn (fs, _) => sql_table fs) ts) $(map sql_table (map (fn (fs, _) => fs) ts)) Example usage: val foo select :: {{Type}} {X: full = t1, Y = t2} ­> keep :: {{Type}} {X = fn r => r.A, Y = fn r => r.B + r.C} 15 ­> {From : $(map sql_table full), ...} ­> sql_query keep