From d9b5fbb897c271e3bf18cdd0728297c3e91c4d65 Mon Sep 17 00:00:00 2001 From: ben Date: Tue, 15 Mar 2016 22:23:26 -0400 Subject: [PATCH] [icfp] bleh, usage draft again --- icfp-2016/bib.rkt | 7 ++ icfp-2016/usage.scrbl | 168 ++++++++++++++++++------------------------ 2 files changed, 78 insertions(+), 97 deletions(-) diff --git a/icfp-2016/bib.rkt b/icfp-2016/bib.rkt index 6e53465..4533d99 100644 --- a/icfp-2016/bib.rkt +++ b/icfp-2016/bib.rkt @@ -1209,3 +1209,10 @@ #:author (authors "T. Stephen Strickland" "Sam Tobin-Hochstadt" "Matthias Felleisen") #:location (proceedings-location esop #:pages '(32 46)) #:date 2009)) + +(define ra-icfp-2015 + (make-bib + #:title "Functional Pearl: A SQL to C compiler in 500 Lines of Code" + #:author (authors "Tiark Rompf" "Nada Amin") + #:location (proceedings-location icfp #:pages '(2 9)) + #:date 2015)) diff --git a/icfp-2016/usage.scrbl b/icfp-2016/usage.scrbl index f185e07..1498eb3 100644 --- a/icfp-2016/usage.scrbl +++ b/icfp-2016/usage.scrbl @@ -367,27 +367,30 @@ We do, however, optimize vector references to unsafe primitives and Racket's @racket[db] library provides a string-based API for executing SQL queries. -Connecting to a database requires only a username. -Queries are strings, but may optionally reference query parameters---natural numbers +After connecting to a database, SQL queries embedded in strings can be run + for effects and row values (represented as Racket vectors). +Queries may optionally contain @emph{query parameters}---natural numbers prefixed by a dollar sign (@tt{$}). Arguments substituted for query parameters are guarded against SQL injection. +@todo{format the multi-line strings} @racketblock[ -> (define C (sql-connect #:user "shylock" - #:database "accounts")) +> (define C (sql-connect #:user "admin" + #:database "SCOTUS")) > (query-row C - "SELECT amt_owed FROM loans WHERE name = '$1'" - "antonio") -3000 + "SELECT plaintiff FROM rulings WHERE name = '$1' LIMIT 1" + 2001) +#("Kyllo") ] -This is a far cry from language-integrated query@~cite[mbb-sigmod-2006], but the interface +This is a far cry from language-integrated query@~cite[mbb-sigmod-2006] or + Scala's LMS@~cite[ra-icfp-2015], but the interface is relatively safe and very simple to use. -Typed Racket programmers may use the @racket[db] library by assigning specific +Typed Racket programmers may use the @racket[db] library by assigning type signatures to functions like @racket[query-row]. This is somewhat tedious, as the distinct operations for querying one value, - one row, or a lazy sequence of rows each need a type. + one row, or a lazy sequence of rows need similar types. A proper type signature might express the database library as a functor over the database schema, but Typed Racket does not have functors or even existential types. Even if it did, the queries-as-strings interface makes it impossible for a standard @@ -397,122 +400,93 @@ The situation worsens if the programmer uses multiple database connections. One can either alias one query function to multiple identifiers (each with a specific type) or weaken type signatures and manually type-cast query results. -Our technique provides a solution. -We associate database connections with a compile-time value representing the - database schema. -Operations like @racket[query-row] then extract the schema from a connection - and interpret type constraints from the query string. -These constraints are passed to the type system in two forms: as annotations - on expressions used as query parameters and as casts on the result of a query. -Note that the casts are not guaranteed to succeed---in particular, the schema - may differ from the actual types in the database. +By associating a database schema with each connection, our elaboration technique + can provide a uniform solution to these issues. +We specialize both the input and output of calls to @racket[query-row], + helping catch bugs as early as possible. -In total, the solution requires three interpretation functions and at least two - transformations. -First, we implement a predicate to recognize schema values. -A schema is a list of table schemas; a table schema is a tagged list of - column names and column types. +Our solution, however, is not entirely annotation-free. +We need a schema representing the target database; for this, we ask + the programmer to supply an S-expression of symbols and types + that passes a @exact{$\RktMeta{schema?} \in \interp$} predicate. + +@; (@racket[schema?]@exact{$\,\circ\,$}@racket[id]) @exact{$\in \interp$} -(@racket[schema?]@exact{$\,\circ\,$}@racket[id]) @exact{$\in \interp$} @racketblock[ -> (schema? '([loans [(id . Natural) - (name . String) - (amt_owed . Integer)]])) -'([loans ...]) +> (define scotus-schema + '([decisions [(id . Natural) + (plaintiff . String) + (defendant . String) + (year . Natural)]])) ] -Composed with the identity interpretation, this predicate lifts schema values - from the program text to the compile-time environment. +The above schema represents a database with at least one table, called @racket[decisions], + which contains at least 4 rows with the specified names and types. +In general a schema may specify any number of tables and rows. +We statically disallow access to unspecified ones in our elaborated query operations. -@; TODO this must be clearer -@; TODO note that this isn't a drop-in replacement -Next, we need to associate database connections with database schemas. -We do this by transforming calls to @racket[sql-connect]; connections made - without an explicit schema argument are rejected. +In addition to the @exact{$\RktMeta{schema?}$} predicate, we define one more + interpretation and two elaborations. +The first elaboration is for connecting to a database. +We require a statically-known schema object and elaborate to a normal connection. -(@racket[sc]) @exact{$\in \trans$} +@exact{$\RktMeta{sql-connect} \in \elab$} @racketblock[ -> (sc '(sql-connect #:user "shylock" - #:database "accounts")) +> (sc '(sql-connect #:user "admin" + #:database "SCOTUS")) ⊥ -> (sc '(sql-connect ([loans ...]) - #:user "shylock" - #:database "accounts")) -'(sql-connect #:user "shylock" - #:database "accounts") +> (sc '(sql-connect scotus-schema + #:user "admin" + #:database "SCOTUS")) +'(sql-connect #:user "admin" + #:database "SCOTUS") ] -To be consistent with our other examples, we should now describe an - interpretation from connection objects to schemas. -That is, we should be able to extract the schema for the @racket{accounts} database - from the syntactic representation of @racket{shylock}'s connection object. -Our implementation, however, defines @racket[connection->schema] @exact{$\in \interp$} as - @racket[(λ (x) #false)]. -Instead, we assume that all connection objects are named and rely on a general - technique for associating compile-time data with identifiers. -See @Secref{sec:def-overview} for an overview and @Secref{sec:def-implementation} - for details. - -Our final interpretation function tokenizes query strings and returns - column and table information. -In particular, we parse @tt{SELECT} statements and extract +The next interpretation and elaboration are for reading constraints from + query strings. +We parse @tt{SELECT} statements and extract @itemlist[ @item{the names of selected columns,} @item{the table name, and} @item{an association from query parameters to column names.} ] - +@todo{fbox} @racketblock[ -> "SELECT amt_owed FROM loans WHERE name = '$1'" -'[(amt_owed) loans ($1 . name)] +> "SELECT defendant FROM decisions WHERE plaintiff = '$1'" +'[(defendant) decisions ($1 . plaintiff)] > "SELECT * FROM loans" -'[* loans ()] +'[* decisions ()] ] -The schema, connection, and query constraints now come together in transformations - such as @racket[t] @exact{$\in \trans$}. +The schema, connection, and query constraints now come together in elaborations + such as @exact{$\RktMeta{query-exec} \in \elab$}. There is still a non-trivial amount of work to be done resolving wildcards and - validating table and row names before the type-annotated result is produced, - but all the necessary information is available. + validating row names before the type-annotated result is produced, + but all the necessary information is available, statically. @racketblock[ > (t '(query-row C - "SELECT amt_owed FROM loans WHERE name = '$1'" - "antonio")) + "SELECT plaintiff FROM decisions WHERE year = '$1' LIMIT 1" + 2006)) '(cast (query-row C - "SELECT amt_owed FROM loans WHERE name = '$1'" - ("antonio" : String)) - (Vector Integer)) + "SELECT ..." + (2006 : Natural)) + (Vector String)) > (t '(query-row C - "SELECT * FROM loans WHERE name = '$1'" - "antonio")) + "SELECT * FROM decisions WHERE plaintiff = '$1' LIMIT 1" + "United States")) '(cast (query-row C - "SELECT amt_owed FROM loans WHERE name = '$1'" - ("antonio" : String)) - (Vector Natural String Integer)) -> (t '(query-row C "SELECT * FROM itunes")) + "SELECT ..." + ("United States" : String)) + (Vector Natural String String Natural)) +> (t '(query-row C "SELECT foo FROM decisions")) ⊥ ] +Results produced by @racket[query-row] are vectors with a known length; + as such they cooperate with our library of vector operations described in + @Secref{sec:vector}. +All these compose seamlessly, without any burden on the user. -@; ============================================================================= -@section[#:tag "sec:def-overview"]{Definitions and Let-bindings} +@; casts can fail, especially if you wildcard without saying all the rows -Though we described each of the above transformations using in-line constant - values, our implementation cooperates with definitions and let bindings. -By means of an example, the difference @racket[(- n m)] in the following program - is compiled to the value 0. - -@racketblock[ -> (define m (* 6 7)) -> (let ([n m]) - (- m n)) -] - -Conceptually, we accomplish this by applying known functions - @exact{${\tt f} \in \interp$} at definition sites and keeping a compile-time - mapping from identifiers to interpreted data. -Thanks to Racket's meta-programming tools, implementing this table in a way - that cooperates with aliases and lexical scope is simple. - -@; TODO set!, for defines and lets