This small web application will keep track of your todo list. It's written in Idris and demonstrates how the dependent type system of Idris can be used to improve abstraction and safety in a web server program.
The advanced proof system embedded in Idris is used to make compile times guarantees about the correctness of the program. The most notable application of this idea can be seen in the SQL package which was written in support of this project. The proof system is used to statically proof correctness properties of the SQL queries generated by the application. Of course, for such a simple website these proofs are overkill, but they could drastically improve the code quality of bigger software projects.
Make sure to install the latest version of the Idris compiler. This package has a dependency on the following packages:
- record_ (standalone)
- effects (bundled with Idris)
- html (standalone)
- file (standalone, wrapper around a single function)
- ferryjs (dependencies: record_)
- event (dependencies: record_, ferryjs)
- http (dependencies: record_, ferryjs, event)
- sql (dependencies: record_, ferryjs, event)
Install these packages manually (see their readme files). Then run:
idris -p effects -p record_ -p ferryjs -p html -p sql -p event -p http -p file --codegen node -o todo.js ./Main.idr
The produced JavaScript program todo.js requires the following external Node.js packages to run:
npm install html-entities pg
The todo.js script accepts the database name, user name and password as command line arguments:
node ./todo.js database-name username password
The database should contain a table named "todo":
CREATE TABLE todo
(
name character varying NOT NULL,
done boolean NOT NULL,
id serial PRIMARY KEY
);Mozilla Public License, v. 2.0