From db2a6886335aada97a6e303b4747cfdd2d15b2d5 Mon Sep 17 00:00:00 2001 From: stefan-hoeck Date: Thu, 9 Nov 2023 18:53:48 +0100 Subject: [PATCH] [ doc ] write a proper README with example app --- .github/workflows/ci-lib.yml | 2 + README.md | 7 +- docs/docs.ipkg | 9 ++ docs/src/README.md | 275 +++++++++++++++++++++++++++++++++++ pack.toml | 9 +- sqlite3.ipkg | 4 +- src/Data/WithID.idr | 21 +++ src/Sqlite3/Cmd.idr | 38 ++++- src/Sqlite3/Parameter.idr | 4 +- test/src/Main.idr | 3 +- test/src/Schema.idr | 29 +--- 11 files changed, 357 insertions(+), 44 deletions(-) mode change 100644 => 120000 README.md create mode 100644 docs/docs.ipkg create mode 100644 docs/src/README.md create mode 100644 src/Data/WithID.idr diff --git a/.github/workflows/ci-lib.yml b/.github/workflows/ci-lib.yml index 680f9b9..8f48739 100644 --- a/.github/workflows/ci-lib.yml +++ b/.github/workflows/ci-lib.yml @@ -37,3 +37,5 @@ jobs: run: pack --no-prompt test sqlite3 - name: Build sqlite3-rio run: pack --no-prompt install sqlite3-rio + - name: Typecheck docs + run: pack --no-prompt typecheck sqlite3-docs diff --git a/README.md b/README.md deleted file mode 100644 index d30b606..0000000 --- a/README.md +++ /dev/null @@ -1,6 +0,0 @@ -# idris2-sqlite3 Idris2 Bindings to the sqlite3 C-API - -This library is based on previous work by -@MarcelineVQ: [idris-sqlite3](https://github.com/MarcelineVQ/idris-sqlite3). - -It is currently under development. diff --git a/README.md b/README.md new file mode 120000 index 0000000..95cf2af --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +docs/src/README.md \ No newline at end of file diff --git a/docs/docs.ipkg b/docs/docs.ipkg new file mode 100644 index 0000000..5d0a932 --- /dev/null +++ b/docs/docs.ipkg @@ -0,0 +1,9 @@ +package sqlite3-docs +version = 0.0.1 +authors = "stefan-hoeck" + +depends = sqlite3-rio + +sourcedir = "src" + +modules = README diff --git a/docs/src/README.md b/docs/src/README.md new file mode 100644 index 0000000..f7f37fb --- /dev/null +++ b/docs/src/README.md @@ -0,0 +1,275 @@ +# idris2-sqlite3 Idris2 Bindings to the sqlite3 C-API + +First and foremost, this library provides +low-level bindings to the SQLite C-API, that can be used by any +Idris projects planning to interact with SQLite databases. In addition, +a domain-specific language (DSL) for writing correctly typed SQL queries and +statements is provided. Finally, derivable marshallers for storing Idris +values in and retrieving them from SQLite databases are provided. + +A lot of this is still work in progress, but several things turned out +quite nice already (in my opinion). Below is a short example application +with some comments. First, some imports: + +```idris +module README + +import Data.WithID +import Derive.Sqlite3 +import Control.RIO.Sqlite3 + +%default total +%language ElabReflection +``` + +We start by defining two SQLite tables: One for employees in +a company, and a second one for organisational units. Employees +are linked to the unit they work in by means of a foreign key, +while each unit has a supervisor, who are themselves employees: + +```idris +public export +Units : Table +Units = + table "units" + [ C "unit_id" INTEGER + , C "name" TEXT + , C "head" INTEGER + ] + +public export +Employees : Table +Employees = + table "employees" + [ C "employee_id" INTEGER + , C "name" TEXT + , C "salary" REAL + , C "unit_id" INTEGER + ] +``` + +As you can see, tables are defined by giving them a name together with +a list of columns. Every column comes with its name and the SQLite type +of the values stored in that column. + +We can now define the commands for creating the two tables: + +```idris +export +createUnits : Cmd TCreate +createUnits = + createTable Units + [ PrimaryKey ["unit_id"] + , AutoIncrement "unit_id" + , ForeignKey Employees ["head"] ["employee_id"] + , NotNull "name" + , Unique ["name"] + ] + +export +createEmployees : Cmd TCreate +createEmployees = + createTable Employees + [ PrimaryKey ["employee_id"] + , AutoIncrement "employee_id" + , ForeignKey Units ["unit_id"] ["unit_id"] + , NotNull "name" + , NotNull "salary" + , NotNull "unit_id" + , Check ("salary" > 0) + ] +``` + +As you can see, column and table constraints are listed in the command +used to create tables. All string literals in the code above are being +checked to actually be proper column names of the table we define. + +In addition, we might want to define a bunch of Idris types for +querying the database as well as for inserting data. We could just +use heterogeneous lists for that (from `Data.List.Quantifiers`, and +this library would be perfectly fine with that, but for results +we use a lot in our code, proper record types might be more +convenient). + +```idris +public export +record OrgUnit (h : Type) where + constructor U + name : String + head : h + +%runElab derive "OrgUnit" [Show, Eq, AsRow] + +public export +record Employee (u : Type) where + constructor E + name : String + salary : Double + unit : u + +%runElab derive "Employee" [Show, Eq, AsRow] +``` + +As you can see, we leave one value in each record type abstract. This +will depend on what kind of information we provide or collect +for the given field. Note also, that we derived an interface of type +`AsRow`, which allows us to convert values of these types from and +to rows in a database table. Let's write the code for inserting +values next: + +```idris +export +insertUnit : OrgUnit Bits32 -> Cmd TInsert +insertUnit = insert Units ["name", "head"] + +export +insertEmployee : Employee Bits32 -> Cmd TInsert +insertEmployee = insert Employees ["name", "salary", "unit_id"] +``` + +When inserting stuff, we use `Bits32` numbers for the identifiers +of foreign keys in the tables. Note, that the record types do not +include a field for the primary keys in the tables. We want these +to be auto-generated by SQLite itself. + +I'm now going to show how to query the database. If we want to fetch +full rows from a table, it is convenient to wrap our record values +in a type called `WithID` if we want to include the identifier +in the list of results. + +```idris +rawEmployee : Query (WithID $ Employee Bits32) +rawEmployee = + SELECT + ["employee_id", "name", "salary", "unit_id"] + [< FROM Employees] + `ORDER_BY` [ASC "salary", ASC "name"] +``` + +The query DSL is designed in such a way that it resembles proper +SQL, while being correctly typed (and checked) by Idris. + +A more useful thing to do would probably be to list the name of each +employee's unit instead of the unit's ID. This requires an `INNER JOIN`, +which is just as easy to set up: + +```idris +employee : Query (WithID $ Employee String) +employee = + SELECT + ["e.employee_id", "e.name", "e.salary", "u.name"] + [< FROM (Employees `AS` "e") + , JOIN (Units `AS` "u") `USING` ["unit_id"] + ] + `WHERE` ("e.salary" > 3000.0) + `ORDER_BY` [ASC "e.salary", ASC "e.name"] +``` + +This example also shows that we can rename the tables and +columns in a query and that we can reference them by these +new names. Here's what happens in case of a typo: + +```idris +failing "Can't find an implementation for IsJust" + employeeFail : Query (WithID $ Employee String) + employeeFail = + SELECT + ["e.employee_id", "e.name", "e.salary", "u.name"] + [< FROM (Employees `AS` "e") + , JOIN (Units `AS` "u") `USING` ["unit_id"] + ] + `ORDER_BY` [ASC "e.sulary", ASC "e.name"] +``` + +The error message might not be very helpful, but at least Idris checks +that we didn't make any mistakes. + +As a final example, let's compute some basic statistics about +the organizational units. Because I'm too lazy to come up with +another record type, we just return a heterogeneous list in +this case, which can be simplified by using the `LQuery` type +alias: + +```idris +unitStats : LQuery [String,Bits32,Double,Double,Double] +unitStats = + SELECT + [ "u.name" + , Count "e.name" `AS` "num_employees" + , Avg "e.salary" `AS` "average_salary" + , Min "e.salary" `AS` "min_salary" + , Max "e.salary" `AS` "max_salary" + ] + [< FROM (Employees `AS` "e") + , JOIN (Units `AS` "u") `USING` ["unit_id"] + ] + `GROUP_BY` ["e.unit_id"] + `ORDER_BY` [ASC "average_salary"] +``` + +Finally, let's run some example code. We are going to use the +`Control.RIO.App` effect type to get proper error handling. +We can wrap and run a list of commands in a single transaction +by using the `cmds` utility. For querying the database, we +can use `query`, which takes a `Query t` argument plus a +natural number corresponding to the maximal number of rows +we want to collect and accumulate in a list. + +```idris +0 Errs : List Type +Errs = [SqlError] + +handlers : All (Handler ()) Errs +handlers = [ printLn ] + +app : App Errs () +app = withDB ":memory:" $ do + cmds $ + [ createUnits + , createEmployees + , insertUnit $ U "Sales" 1 + , insertUnit $ U "R&D" 2 + , insertUnit $ U "HR" 3 + , insertEmployee $ E "Sarah" 8300.0 1 + , insertEmployee $ E "Ben" 8000.0 2 + , insertEmployee $ E "Gil" 7750.0 3 + , insertEmployee $ E "Cathy" 3000.0 1 + , insertEmployee $ E "John" 3100.0 1 + , insertEmployee $ E "Abby" 3000.0 2 + , insertEmployee $ E "May" 3100.0 2 + , insertEmployee $ E "Brian" 3000.0 2 + , insertEmployee $ E "Benny" 3100.0 2 + , insertEmployee $ E "Rob" 3100.0 3 + , insertEmployee $ E "Zelda" 3100.0 3 + , insertEmployee $ E "Gundi" 2050.0 1 + , insertEmployee $ E "Valeri" 5010.0 1 + , insertEmployee $ E "Ronja" 4010.0 1 + ] + es <- query employee 1000 + traverse_ printLn es + ss <- query unitStats 1000 + traverse_ printLn ss + +main : IO () +main = runApp handlers app +``` + +If you are using [pack](https://github.com/stefan-hoeck/idris2-pack) for +managing and installing Idris dependencies, you can compile and run +this example program simply by typing `pack exec docs/src/README.md` +from this project's root directory. + +## Next Steps + +I'm planning to write a proper tutorial for this library explaining +in detail how to use it and also discussing some of the design +decisions that led to the current implementation. This is still +work in progress, so stay tuned. + +## Credits + +This library is based on previous work by +@MarcelineVQ: [idris-sqlite3](https://github.com/MarcelineVQ/idris-sqlite3). + + diff --git a/pack.toml b/pack.toml index 10e8c94..392c4db 100644 --- a/pack.toml +++ b/pack.toml @@ -9,8 +9,7 @@ type = "local" path = "sqlite3-rio" ipkg = "sqlite3-rio.ipkg" -[custom.all.bytestring] -type = "git" -url = "https://github.com/stefan-hoeck/idris2-bytestring" -commit = "latest:main" -ipkg = "bytestring.ipkg" +[custom.all.sqlite3-docs] +type = "local" +path = "docs" +ipkg = "docs.ipkg" diff --git a/sqlite3.ipkg b/sqlite3.ipkg index b6822df..f5225fe 100644 --- a/sqlite3.ipkg +++ b/sqlite3.ipkg @@ -11,7 +11,9 @@ depends = base >= 0.6.0 sourcedir = "src" -modules = Derive.Sqlite3 +modules = Data.WithID + + , Derive.Sqlite3 , Derive.Sqlite3.AsCell , Derive.Sqlite3.AsRow diff --git a/src/Data/WithID.idr b/src/Data/WithID.idr new file mode 100644 index 0000000..f1d328b --- /dev/null +++ b/src/Data/WithID.idr @@ -0,0 +1,21 @@ +module Data.WithID + +import Data.List.Quantifiers +import Derive.Sqlite3 + +%default total +%language ElabReflection + +public export +record WithID (a : Type) where + constructor MkWithID + id : Bits32 + value : a + +%runElab derive "WithID" [Show,Eq,Ord] + +public export +AsRow a => AsRow (WithID a) where + rowTypes = INTEGER :: RowTypes a + toRow (MkWithID i v) = toCell i :: toRow v + fromRow (h::t) = [| MkWithID (fromCell h) (fromRow t) |] diff --git a/src/Sqlite3/Cmd.idr b/src/Sqlite3/Cmd.idr index 90b0dbe..08029dc 100644 --- a/src/Sqlite3/Cmd.idr +++ b/src/Sqlite3/Cmd.idr @@ -189,7 +189,7 @@ data From : (s : Schema) -> Type where ||| Tag indicating, whether results should be sorted in ascending ||| or descending order. public export -data AscDesc = NoAsc | ASC | DESC +data AscDesc = NoAsc | Asc | Desc ||| Different collations used during ordering. ||| @@ -207,6 +207,18 @@ record OrderingTerm (s : Schema) where coll : Collation tpe asc : AscDesc +public export %inline +ASC : Expr s t -> OrderingTerm s +ASC x = O x None Asc + +public export %inline +DESC : Expr s t -> OrderingTerm s +DESC x = O x None Desc + +public export %inline +COLLATE : (o : OrderingTerm s) -> Collation o.tpe -> OrderingTerm s +COLLATE o c = {coll := c} o + public export record GroupingTerm (s : Schema) where constructor G @@ -214,6 +226,15 @@ record GroupingTerm (s : Schema) where expr : Expr s tpe coll : Collation tpe +namespace GroupingTerm + public export %inline + fromString : + {s : Schema} + -> (col : String) + -> {auto 0 p : IsJust (FindSchemaCol col s)} + -> GroupingTerm s + fromString col = G (fromString col) None + public export %inline ord : GroupingTerm s -> OrderingTerm s ord (G x c) = O x c NoAsc @@ -224,13 +245,14 @@ record NamedExpr (s : Schema) (t : SqliteType) where expr : Expr s t name : String -public export %inline -fromString : - {s : Schema} - -> (col : String) - -> {auto 0 p : IsJust (FindSchemaCol col s)} - -> NamedExpr s (SchemaColType col s) -fromString col = C col `AS` "" +namespace NameExpr + public export %inline + fromString : + {s : Schema} + -> (col : String) + -> {auto 0 p : IsJust (FindSchemaCol col s)} + -> NamedExpr s (SchemaColType col s) + fromString col = C col `AS` "" public export ExprColumns : {ts : _} -> LAll (NamedExpr s) ts -> List Column diff --git a/src/Sqlite3/Parameter.idr b/src/Sqlite3/Parameter.idr index 225911e..aea2904 100644 --- a/src/Sqlite3/Parameter.idr +++ b/src/Sqlite3/Parameter.idr @@ -277,8 +277,8 @@ encodeFrom (x :< y) = do asc : AscDesc -> String asc NoAsc = "" -asc ASC = "ASC" -asc DESC = "DESC" +asc Asc = "Asc" +asc Desc = "Desc" collate : Collation t -> String collate None = "" diff --git a/test/src/Main.idr b/test/src/Main.idr index e15c1a8..616930a 100644 --- a/test/src/Main.idr +++ b/test/src/Main.idr @@ -4,6 +4,7 @@ import Control.RIO.Sqlite3 import Data.Buffer.Indexed import Data.ByteString import Data.List.Quantifiers +import Data.WithID import Enum import Schema @@ -58,7 +59,7 @@ app = withDB ":memory:" $ do ms <- query (mol TRUE) 1000 traverse_ printLn ms fs <- query (file TRUE `LIMIT` 20) 1000 - traverse_ (putStrLn . encodeBytes . content . item) fs + traverse_ (putStrLn . encodeBytes . content . value) fs es <- query employee 1000 traverse_ printLn es hs <- query heads 1000 diff --git a/test/src/Schema.idr b/test/src/Schema.idr index 56440e1..81319e5 100644 --- a/test/src/Schema.idr +++ b/test/src/Schema.idr @@ -1,5 +1,6 @@ module Schema +import Data.WithID import Data.Buffer.Indexed import Data.ByteString import Data.List.Quantifiers @@ -129,20 +130,6 @@ record File where %runElab derive "File" [Show, Eq, AsRow] -public export -record Item (i : Type) where - constructor I - id : Bits32 - item : i - -%runElab derive "Schema.Item" [Show, Eq] - -public export -AsRow i => AsRow (Item i) where - rowTypes = INTEGER :: RowTypes i - toRow (I id itm) = toCell id :: toRow itm - fromRow (id::t) = [| I (fromCell id) (fromRow t) |] - -------------------------------------------------------------------------------- -- Create -------------------------------------------------------------------------------- @@ -168,7 +155,7 @@ insertFile = insert Files ["content"] -------------------------------------------------------------------------------- export -mol : Expr [ Query (Item Molecule) +mol : Expr [ Query (WithID Molecule) mol x = SELECT ["molecule_id", "name", "casnr", "molweight", "type"] @@ -176,11 +163,11 @@ mol x = `WHERE` x export -file : Expr [ Query (Item File) +file : Expr [ Query (WithID File) file x = SELECT ["file_id", "content"] [ 3000.0) - `ORDER_BY` [O "e.salary" None ASC, O "e.name" NOCASE ASC] + `ORDER_BY` [ASC "e.salary", ASC "e.name"] export unitStats : LQuery [String,Bits32,Double,Double,Double] @@ -203,9 +190,9 @@ unitStats = [< FROM (Employees `AS` "e") , JOIN (Units `AS` "u") `USING` ["unit_id"] ] - `GROUP_BY` [G "e.unit_id" None] + `GROUP_BY` ["e.unit_id"] `HAVING` ("num_employees" > 3) - `ORDER_BY` [O "average_salary" None ASC] + `ORDER_BY` [ASC "average_salary"] export heads : Query (OrgUnit String) @@ -225,7 +212,7 @@ nonHeads = , OUTER_JOIN (Units `AS` "u") `ON` ("e.employee_id" == "u.head") ] `WHERE` IS NULL "u.head" - `ORDER_BY` [O "e.name" None ASC] + `ORDER_BY` [ASC "e.name"] export tuples : LQuery [String,Double,Double,MolType]