An Idris example using a database with JDBC and idris-jvm

JdbcExample.idr

module Main

import IdrisJvm.IO

namespace ResultSet

  ResultSet : Type
  ResultSet = JVM_Native $ Interface "java/sql/ResultSet"

  next : ResultSet -> JVM_IO Bool
  next = invokeInstance "next" (ResultSet -> JVM_IO Bool)

  getInt : ResultSet -> String -> JVM_IO Int
  getInt = invokeInstance "getInt" (ResultSet -> String -> JVM_IO Int)

  getString : ResultSet -> String -> JVM_IO String
  getString = invokeInstance "getString" (ResultSet -> String -> JVM_IO String)

namespace PreparedStatement
  PreparedStatement : Type
  PreparedStatement = JVM_Native $ Interface "java/sql/PreparedStatement"

  setInt : PreparedStatement -> Int -> Int -> JVM_IO ()
  setInt = invokeInstance "setInt" (PreparedStatement -> Int -> Int -> JVM_IO ())

  setString : PreparedStatement -> Int -> String -> JVM_IO ()
  setString = invokeInstance "setString" (PreparedStatement -> Int -> String -> JVM_IO ())

  executeUpdate : PreparedStatement -> JVM_IO Int
  executeUpdate = invokeInstance "executeUpdate" (PreparedStatement -> JVM_IO Int)

  executeQuery : PreparedStatement -> JVM_IO ResultSet
  executeQuery = invokeInstance "executeQuery" (PreparedStatement -> JVM_IO ResultSet)

  close : PreparedStatement -> JVM_IO ()
  close = invokeInstance "close" (PreparedStatement -> JVM_IO ())

namespace Connection

  Connection : Type
  Connection = JVM_Native $ Interface "java/sql/Connection"

  prepareStatement : Connection -> String -> JVM_IO PreparedStatement
  prepareStatement = invokeInstance "prepareStatement" (Connection -> String -> JVM_IO PreparedStatement)

  commit : Connection -> JVM_IO ()
  commit = invokeInstance "commit" (Connection -> JVM_IO ())

  close : Connection -> JVM_IO ()
  close = invokeInstance "close" (Connection -> JVM_IO ())

namespace DriverManager

  DriverManagerClass : JVM_NativeTy
  DriverManagerClass = Class "java/sql/DriverManager"

  getConnection : String -> JVM_IO Connection
  getConnection = invokeStatic DriverManagerClass "getConnection" (String -> JVM_IO Connection)

createQuery : String
createQuery = "CREATE TABLE TODO(id int primary key, description varchar(255))"

insertQuery : String
insertQuery = "INSERT INTO TODO (id, description) values (?,?)"

selectQuery : String
selectQuery = "select * from TODO"

addTodo : Connection -> Int -> String -> JVM_IO ()
addTodo connection id todo = do
  insertStmt <- prepareStatement connection insertQuery
  setInt insertStmt 1 id
  setString insertStmt 2 todo
  executeUpdate insertStmt
  PreparedStatement.close insertStmt

printRow : ResultSet -> JVM_IO ()
printRow rs = do
  id <- getInt rs "id"
  desc <- getString rs "description"
  printLn $ "Id: " ++ show id ++ ", TODO: " ++ desc

main : JVM_IO ()
main = do
  connection <- DriverManager.getConnection "jdbc:derby:memory:testDB;create=true"

  createStmt <- prepareStatement connection createQuery
  executeUpdate createStmt
  PreparedStatement.close createStmt

  addTodo connection 1 "Learn Haskell"
  addTodo connection 2 "Learn Idris"

  selectStmt <- prepareStatement connection selectQuery
  rs <- executeQuery selectStmt

  while (next rs) $ printRow rs

  PreparedStatement.close selectStmt
  Connection.close connection

run.txt

$ idrisjvm JdbcExample.idr -o target

$ java -cp target:/path/to/idris-jvm-runtime-1.0-SNAPSHOT.jar:/path/to/derby.jar main.Main
"Id: 1, TODO: Learn Haskell"
"Id: 2, TODO: Learn Idris"