suzanne.soy/trivial
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[icfp] longer db explanation

Browse Source
This commit is contained in:
ben 2016-03-08 13:24:53 -05:00
parent 8250705ecb
commit 8293370a80
2 changed files with 56 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
icfp-2016/implementation.scrbl
View File

@ -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.
}
]

57
icfp-2016/usage.scrbl
View File

@ -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