From 8293370a807110260d3887f116a0ab6953b0fd76 Mon Sep 17 00:00:00 2001
From: ben <benjaminlgreenman@gmail.com>
Date: Tue, 8 Mar 2016 13:24:53 -0500
Subject: [PATCH] [icfp] longer db explanation

---
 icfp-2016/implementation.scrbl | 40 ------------------------
 icfp-2016/usage.scrbl          | 57 +++++++++++++++++++++++++++++++++-
 2 files changed, 56 insertions(+), 41 deletions(-)

diff --git a/icfp-2016/implementation.scrbl b/icfp-2016/implementation.scrbl
index ddd781e..f8b7683 100644
--- a/icfp-2016/implementation.scrbl
+++ b/icfp-2016/implementation.scrbl
@@ -15,46 +15,6 @@
 
 
 
-@section{Database}
-
-Note: Typed Racket users can already specialize functions from the @tt{db} library
- by giving them exact types in an import statement:
-
-@racketblock[
-  (require/typed db
-    (#:opaque Connection connection?)
-    (postgresql-connect (->* () (#:user String #:database String) Connection))
-    (query-row (-> Connection String Any * (Vector Natural String)))
-    (query-maybe-row (-> Connection String Any * (Option (Vector Natural String))))
-    ....)
-]
-
-The above statement asserts that @racket[query-row] only returns rows containing
- a natural number followed by a string.
-To work with multiple tables in the same module, a programmer can re-import
- @racket[db] functions using a different name and type.
-
-@todo{cohernet table names}
-@racketblock[
-  (require/typed (prefix-in w: db)
-    (w:query-row (-> Connection String Any * (Vector Natural String))))
-
-  (require/typed (prefix-in s: db)
-    (s:query-row (-> Connection String Any * (Vector Natural Natural))))
-]
-
-@todo{Other languages? also follow this approach}
-
-The benefits of our approach are:
-@itemlist[
-  @item{
-    Single point of control for database types, instead of spreading types
-    across identifiers in the @racket[require/typed] statement.
-  }
-  @item{
-    Compile-time validation of query strings.
-  }
-]
 
 
 
diff --git a/icfp-2016/usage.scrbl b/icfp-2016/usage.scrbl
index b5f32ab..cdde9e9 100644
--- a/icfp-2016/usage.scrbl
+++ b/icfp-2016/usage.scrbl
@@ -4,7 +4,62 @@
 
 @; regexp-match
 @; format
-@; db
 @; math
 @; vectors
 @; arity
+
+
+@section{Database}
+@; db
+
+In the years since 2004, language-integrated query has been a popular
+ topic.
+Languages like Scala, @tt{C#}, and @tt{F*} have fast and type-safe
+ interfaces for working with SQL databases.
+
+@; SO WHAT ARE WE DOING HERE
+
+@; Hey, Racket / typed Racket does not fit with the overalll story of
+@; dependent-like types
+
+Racket's @racket[db] library provides a direct connection to the database,
+ modulo some important safety checks.
+
+Typed Racket programmers may use the @racket[db] library by giving type signatures
+ specialized to their needs.
+For example, the statement below asserts that @racket[query-row] always returns
+ a natural number and a string.
+In contrast, @racket[query-maybe-row] can optionally fail, but otherwise returns
+ a natural number and a string.
+
+@racketblock[
+  (require/typed db
+    (#:opaque Connection connection?)
+    (sql-connect (->* () (#:user String #:database String) Connection))
+    (query-row (-> Connection String Any * (Vector Natural String)))
+    (query-maybe-row (-> Connection String Any * (Option (Vector Natural String))))
+    ....)
+]
+
+To manage additional tables, the programmer can re-import @racket[db] identifiers
+ with a fresh name and type signature.
+
+@todo{coherent example}
+@racketblock[
+  (require/typed (prefix-in w: db)
+    (w:query-row (-> Connection String Any * (Vector Natural String))))
+
+  (require/typed (prefix-in s: db)
+    (s:query-row (-> Connection String Any * (Vector Natural Natural))))
+]
+
+This approach works, but is tedious and error-prone.
+Our contribution is to associate a type signature with database connections.
+Calls to generic operations like @racket[query-row] are then specialized to
+ the exact result type.
+
+@; PERKS
+@; - Single point-of-control
+@; - lightweight
+@; - no changes to underlying library / type system
+@; - compile-time validation of query strings