I’ve been playing around with making a dependently typed language. It’s based upon Martin-Löf Type Theory (commonly just called Type Theory, TT). Turns out that implementing a dependent type system is a great way to learn how to use one!

I had written code to translate from my toy languages’ terms into TT - but I wanted a compiler, so that I could execute it somewhere outside of the evaluator/normaliser. I started thinking about how I could possibly compile TT to JavaScript but then I realised that Idris already handles code generation from TT:

Well, I only wanted to compile to a single target, but wow, I’ll take all four please! If only I could reuse the Idris backend…

So a few weeks ago I turned Idris into a Cabal library so I could just depend on it in my project and use the code generators. I just had to move all of the files around and add a Library section to idris.cabal. Easy!

The commit was only merged sometime today so there’s no Hackage release yet. If you want to play with it, you should do something like the following:

git clone https://github.com/idris-lang/Idris-dev.git
mkdir my-language
cd my-language
cabal sandbox init
cabal sandbox add-source ../Idris-dev

Which allows adding a dependency on the Idris library and have it compile from master.

Here is a short and incomplete example of using the library:

import IRTS.Compiler
import Idris.AbsSyntax
import Idris.Core.TT
import Idris.Delaborate
import Idris.ElabDecls
import Idris.ElabTerm
import Idris.Parser

run :: (PTerm -> PDecl) -> TT Name -> TT Name -> Idris ()
run makeDecl program runProgram = do
  ddir <- runIO $ getIdrisLibDir
  addImportDir $ ddir </> "prelude"
  addImportDir $ ddir </> "base"
  elabPrims
  _ <- loadModule stdout "Builtins"
  _ <- loadModule stdout "Prelude"
  pterm <- fmap (flip delab program) getIState
  elabDecls toplevel [makeDecl pterm]
  compile ViaNode "wow.js" runProgram

The first 6 lines of run setup the Idris standard library, allowing us to access primitive IO functions. The next line “delaborates” our custom TT (defined in program) back to Idris terms. The next line elaborates those Idris terms (yes, strange since we just delaborated; but the compiler needs terms to be in scope, using the elaborator is the easiest way to do it). The final line writes a wow.js node.js program!

So, if you want to make a dependently typed language, Idris has a great backend waiting for you to reuse (theoretically it doesn’t even have to be dependently typed; it just has to compile to TT). The Idris backend will handle compiling to JavaScript, Java, C, LLVM and any other code generators which could be added later. You’ll be free to focus on language features!