SQL.idr

module Interactive.SQL
 
import Derive.Sqlite3
import Control.RIO.Sqlite3
import Control.RIO.App
import Control.RIO
import Data.Sigma
 
import Data.Container
import Data.Container.Morphism
import Data.Container.Kleene
import Data.Container.Descriptions.Maybe
import Data.Maybe
import Data.Either
import Data.Sum
 
import Data.String.Parser
 
import JSON.Derive
import System.File
 
%language ElabReflection
%default total
 
%hide Data.List.Alternating.infixr.(<+)
%hide Data.List.Alternating.infixl.(<+)
%hide Data.String.Extra.infixr.(<+)
%hide Data.String.Extra.infixl.(+>)

Do demonstrate how to use container morphisms to build software, I build a simple to-do app using the building blocs we’ve seen.

A to-do app is a piece of software aimed to help users store and recall items representing actions to take in the future. I will implement this app as a

Datatypes

First we describe datatypes, we need a couple of base definitions, the first is an ID type for uniquely identifying todo items.

public export
ID : Type
ID = Integer

A todo item has a boolean status, either it is completed, or it is not done yet.

-- And a status to indicate if the item is marked as done.
data Status = Done | NotDone
 
toBool : Status -> Bool
toBool Done = True
toBool NotDone = False
 
fromBool : Bool -> Status
fromBool True = Done
fromBool False = NotDone

A todo item is a record of an ID to identify it, a content string for the text entered by the user, and a Status to know if it’s been marked done or not.

record Todo where
  constructor MkTodo
  id : ID
  content : String
  status : Status

The app will accept commands that will perform operations relevant to the app’s functionality, in particular, we need to be able to create a todo item, delete an item using its ID, mark an item completed using its ID and obtain the list of all todo items.

data TodoCommand
  = Create String
  | Delete ID
  | MarkComplete ID
  | RetrieveAll

For each of those commands, we provide the type of the answers sent back to the clients from the servers. Most commands do not result in a value sent back to the client, but only perform a side effect, and so the type of the returned value is Unit. Only RetrieveAll returns a value to the user, and therefore its type is Table Todo. Table is the type of tables returned by SQL queries, and Todo is the type we defined above.

CmdReturn : TodoCommand -> Type
CmdReturn (Create str) = Unit
CmdReturn (Delete i) = Unit
CmdReturn (MarkComplete i) = Unit
CmdReturn RetrieveAll = Table Todo

SQL setup

For this app, I will use SQL bindings. They require some boilerplate to work with the types defined above, once the bindings are defined, we can seamlessly interact with the SQL database using the messages we defined.

First the boilerplate to serialise and deserialise types into database fields and rows:

%runElab derive "TodoCommand" [Show,Eq,ToJSON,FromJSON]

FromCell Status where
  fromCellType = INTEGER
  fromCell = map fromBool . fromCell

ToCell Status where
  toCellType = INTEGER
  toCell = toCell . toBool

FromRow Todo where
  fromRowTypes = [INTEGER, TEXT, INTEGER]
  fromRow [i, c, s] = do id <- fromCell i
                         cont <- fromCell c
                         stat <- fromCell s
                         pure (MkTodo id cont stat)
ToRow Todo where
  toRowTypes = [INTEGER, TEXT, INTEGER]
  toRow (MkTodo id cont stat) = [toCell (cast {to = Int32} id), toCell cont, toCell stat]

-- A valid query is one with a type that has the appropriate instances
-- for row conversions
record ValidQuery where
  constructor MkValidQuery
  0 ty : Type
  tr : ToRow ty
  qy : Query ty
  {auto 0 chk : ToRowTypes ty = FromRowTypes ty}

-- We can run any valid query and obtain the list of rows for that query
runValid : Has SqlError e => DB => (x : ValidQuery) -> App e (Table (x .ty))
runValid (MkValidQuery ty tr qy ) = queryTable qy 1000

-- The schema of our database. We onlye 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 setup the table
createTodos : Cmd TCreate
createTodos =
  IF_NOT_EXISTS $ CREATE_TABLE Todos
    [ PRIMARY_KEY   ["todo_id"]
    , AUTOINCREMENT  "todo_id"
    , NOT_NULL       "content"
    , NOT_NULL       "status"
    ]

-- SQL command to add an item to the todo table
addTodoItem : String -> Cmd TInsert
addTodoItem str = INSERT Todos ["content", "status"] (val str :: 0 :: [])

-- SQL command to delete an item from the todo table
deleteItem : Bits32 -> Cmd TDelete
deleteItem i = DELETE Todos ("todo_id" == val i)

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

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

Containers for the app

Next, we need to figure out what are the APIs that we are going to use, and how they are represented as containers.

First

-- The CLI is represented as a container that expects strings as input
-- and returns strings as output.
CLI : Container
CLI = String :- String
 
-- AppOp is the abstract API of our app, we take in commands, and returns
-- either unit, or tables from queries. Will run in FM.
AppOp : Container
AppOp = (!>) TodoCommand CmdReturn
 
-- Interface for database commands. Commands only perform side-effects so the
-- results are always Unit
DBCmd : Container
DBCmd = Σ CmdType Cmd :- ()
 
-- Interface of a database queries. Queries always return tables of a matching type
0 DBQry : Container
DBQry = (x : ValidQuery) !> Table x.ty
 
----------------------------------------------------------------------------------
-- Containers Morphisms                                                         --
----------------------------------------------------------------------------------
 
-- The errors that our program will deal with
0 Errs : List Type
Errs = [SqlError]
 
-- The monad in which we run our program as an endofunctor in Cont
0 FM : Container -> Container
FM x = F (App Errs) x
 
---------------------------------
-- Running database operations --
---------------------------------
 
-- Running a command as a costate
CmdCostate : DB => Costate (FM DBCmd)
CmdCostate = costate (\x => cmd {t = x.π1} x.π2)
 
-- Running a query as a costate
DBQueryCostate : DB => Costate (FM DBQry)
DBQueryCostate = costate runValid
 
-- Running either a command or a query on a database as a costate
DBCostate : DB => Costate (FM (DBCmd + DBQry))
DBCostate = distrib_plus {f = App Errs, a = DBCmd, b = DBQry}
         |> CmdCostate + DBQueryCostate |> dia
 
---------------------------------------
-- Interacting with the command line --
---------------------------------------
 
-- We need a parser to parse command line arguments and translate them into
-- internal Todo commands.
cmdParser : Parser TodoCommand
cmdParser = assert_total $
            string "create" *> spaces *> char '"' *> Create <$> takeWhile (/= '"')
        <|> string "done" *> spaces *> MarkComplete <$> cast <$> natural
        <|> string "delete" *> spaces *> Delete <$> cast <$> natural
        <|> string "print" *> pure RetrieveAll
 
parseInput' : String -> Maybe TodoCommand
parseInput' str = eitherToMaybe $ map fst $ parse cmdParser str
 
-- Convert a string-based api into the AppOp interface
-- MaybeA is the error monad where all errors need to be handled
cliParser : CLI =%> MaybeAll AppOp
cliParser = MkMorphism parseInput' printOutput
  where
    printResult : (v : TodoCommand ** CmdReturn v) -> String
    printResult (RetrieveAll ** b)  = prettyTable b
    printResult (MarkComplete id ** y) = "done"
    printResult (Create content ** y) = "done"
    printResult (Delete id ** y)  = "deleted \{show id}"
 
    printOutput : (x : String) -> (All CmdReturn (parseInput' x)) -> String
    printOutput x y with (parseInput' x)
      printOutput x Nay | Nothing = "could not parse '\{x}'"
      printOutput x (Yay y) | (Just z) = printResult (z ** y)
 
-- The parser lifted into effectful bidirectional programs
-- Note that the parser itself does not concern itself with effects but
-- we can lift it to make to compatible with effectful programs.
parser : FM CLI =%> FM (MaybeAll AppOp)
parser = f_functor cliParser
 
---------------------------------------
-- Converting to database operations --
---------------------------------------
 
-- Converting from internal app commands to database commands
-- Again, notice that this is a pure interface, but the monad on containers
-- will make this compatible with the rest of the infrastructure.
OpToDB : AppOp =%> DBCmd + DBQry
OpToDB = MkMorphism convertCommand convertBack
  where
    convertCommand : TodoCommand -> Σ CmdType Cmd + ValidQuery
    convertCommand (Create str) = <+ (_ ## addTodoItem str)
    convertCommand (Delete i) = <+ (_ ## deleteItem (cast i))
    convertCommand (MarkComplete i) = <+ (_ ## itemMarkDone (cast i))
    convertCommand RetrieveAll = +> MkValidQuery _ %search getAllItems
 
    convertBack : (x : TodoCommand) -> (DBCmd + DBQry).pos (convertCommand x) ->
                  CmdReturn x
    convertBack (Create str) y = ()
    convertBack (Delete i) y = ()
    convertBack (MarkComplete i) y = ()
    convertBack RetrieveAll y = y
 
-- Commands translated to database operations lifted into the correct monads
-- We lift our translatin to database operation through both FM and MaybeA
commands : DB => FM (MaybeAll AppOp) =%> MaybeAll (FM (DBCmd + DBQry))
commands = distribMaybeAF {a = AppOp} |> map_MaybeAll (f_functor OpToDB)
 
-- The application itself as a Costate of FM CLI
-- - First run the parser
-- - Then convert commands into database operations
-- - Then run the database
appCont : DB => Costate (FM CLI)
appCont = parser |> commands  |> map_MaybeAll DBCostate |> maybeAUnit
 
----------------------------------------------------------------------------------
-- Running the app as a REPL                                                    --
----------------------------------------------------------------------------------
 
partial
repl : HasIO io => (String -> io String) -> io ()
repl f = do
  line <- getLine
  output <- f line
  putStrLn output
  repl f
 
-- Running the repl with our String -> String function extracted from the
-- costate `Costate (FM CLI)`
partial
app : DB => App Errs Unit
app = repl (extract appCont)
 
-- Running the database commands to setup an initial state
partial
runDB : App Errs Unit
runDB = withDB ":memory:" $
        cmd createTodos *> app
 
-- Running the main app using RIO
partial
main : IO ()
main = runApp [ printLn ] runDB