Connect to SQL

An application is nothing without data storage, the most straight forward way to add data storage to you app is to translate any message into a series of SQL queries, and report back the result of running that query to the caller. This is what stellar-sql helps you do.

Adding the dependency

In your .ipkg file, add stellar-sql as a dependency, you depends field should look something like this:

depends = stellar-api, stellar-sql

Recompile with pack build to pull the dependency and start coding.

Start defining your queries

Defining your queries is actually unrelated to the functionality offered by stellar. Stellar-sql relies on idris2-sqlite3 to define queries. What follows explain how to setup the library to use it via stellar.

First we need to define our database schema, an initialise it.

-- The schema of our database. We only have
-- a single table with all the todo items.
Todos : SQLTable
Todos =
  table "todos"
    [ C "todo_id" INTEGER
    , C "content" TEXT
    , C "status"  BOOL
    ]

-- We hard-code a SQL command to create our table. This is going to
-- be called when we start the application
export
createTodos : Cmd TCreate
createTodos =
  IF_NOT_EXISTS $ CREATE_TABLE Todos
    [ PRIMARY_KEY   ["todo_id"]
    , AUTOINCREMENT  "todo_id"
    , NOT_NULL       "content"
    , NOT_NULL       "status"
    ]

The type of createTodos is a Cmd, this type comes from idris2-sqlite3 and represent commands that do not themselves return values.

With this table, we can define the command to insert a new todo item.

addTodoItem : TodoData -> Cmd TInsert
addTodoItem str = INSERT Todos ["content", "status"] [val (get' "content" String str), val NotDone]

INSERT here is a function that biulds a Cmd, Todos refers to the database schema we just defined, ["content", "status"] select what fields we are inserting in and [val (get' "content" String str), val NotDone] insert the values. val converts from our idris types to the types expected by SQLite3.

We do the same for marking an item done.

-- SQL command to mark an item done
itemMarkDone : ID -> Cmd TUpdate
itemMarkDone i = UPDATE Todos ["status" .= True] ("todo_id" == val i)

And for obtaining the list of all items

-- SQL query to obtain all the todo items
getAllItems : Query DBTodoItem
getAllItems = SELECT ["todo_id", "content", "status"] [< FROM Todos]

getAllItems is a Query, this means it will return a table, the type of the table returned is given by the columns selected, here todo_id, content and status.

Converting our queries into API-transformers

So far, we only dealt with SQL-specific knowledge, next we need to translate sql queries into API-transformers that Stellar can manipulate.

Whenever interacting with SQLite3, Stellar expects you to provide an API-transformer that maps to the SQL API. The SQL API handles both commands and queries and ensures the return type of a query matches the table selected.

The full definition of the `SQL` API in Stellar

This might be too much to digest in one go, but here is the definiton of the `SQL` api in stellar. It's a choice of two APIs! the first is the API related to _commands_, the second is the API related to _queries_.

Commands only have a return type when they are paired with a `RETURNING` statement. Sql queries have a return type that matches the column selected in the table queried.

``` DBCmd : API DBCmd = (s : Σ CmdType (\t => Σ Type (Statement t))) !> s.π2.π1 DBQry : API DBQry = (x : ValidQuery) !> Table x.ty SQL : API SQL = DBCmd + DBQry ```

Because SQL is a choice of either commands or queries, we need to pick which one we are doing, thankfully this is fairly mechanical, for a Cmd we pick left, the operator for going left is <+. CreateCmd as an API-transformer is therefore picking the left side of the SQL API and passing in the command addTodoItem.

Before we execute the command, we modify the query to add a RETURNING statement to extract the id of the item added and return it to the caller:

createCmd : CREATE =&> SQL
createCmd = !! \ item => <+ (TInsert ## ID ## (addTodoItem item `RETURNING` ["todo_id"]))
                      ## id

Mapping responses is trivial since we simply pass long the ID obtained from inserting the element, the identity function id does just that.

We repeat the same process for marking an item done. It’s a Cmd therefore we select <+ and then pass the command as an SQL operation. The responses from SQL are merely passed along without change.

doneCmd : DONE =&> SQL
doneCmd = !! \ inc => <+ (TUpdate ## () ## itemMarkDone inc)
                   ## id

To obtain all the elements of the database, we perform a query, this is using the right of the SQL API, and so to select it we use the +> operator. Like before, pass the query getAllItems, wrapped in a ValidQuery type, the type of messages expected by SQL queries.

getAllCmd : GET_ALL =&> SQL
getAllCmd = !! \ inc => +> MkValidQuery DBTodoItem getAllItems
                     ## rows

The return type of the sql query is a Table, but the application’s API expects a List TodoItem, so we need to translat from SQL table to lists with the rows function.

Combining all SQL queries

Once every message from the app has been translated into a SQL API, we can combine all API-transformers into one that works for the App’s API. Remember that the App’s API is defined as a choice of every sub-API:

TODO_APP : API
TODO_APP = CREATE + (DONE + GET_ALL)

Stellar provides a function sumAll which takes a list of API-transformers with a common target, here SQL and combines their source with +. Since our Todo app’s API is a series of choices we can use it to automatically dispach messages from the app’s API to SQL using our previously defined API-transformers.

appToSQL : TODO_APP =&> SQL
appToSQL
  = sumAll
  [ createCmd
  , doneCmd
  , getAllCmd
  ]