I wrote a Todo application in Idris that compiles to Javascript (https://github.com/leon-vv/Todo https://github.com/leon-vv/Todo). I used the dependent type sys

I wrote a Todo application in Idris that compiles to Javascript (https://github.com/leon-vv/Todo https://github.com/leon-vv/Todo). I used the dependent type system of Idris to embed a small part of SQL in Idris, which means the type system can proof certain things about my queries (for example that fields accessed are actually part of the (joined) tables).