BAM Weblog

This Blog Uses Idris

Brian McKenna — 2015-02-12

I am not using node.js to generate this blog. I am now using Idris! I’ve chucked the source up on GitHub.

I wanted to be the first to use a dependently typed compiler to generate my blog. From what I can tell, I was beat by just a couple of weeks.

Sadly, there are no interesting uses of dependent types used yet but one interesting thing I worked on was using Nix to build Idris packages. I worked on and packaged:

I also had to create a package to wrap some POSIX functions, such as listing the contents of a directory and checking if a file exists.

To build my program I can just open up a nix-shell from a dummy expression:

with import <nixpkgs> { };
with import <idrispkgs> { };

runCommand "dummy" {
  buildInputs = [
    (idrisWithPackages [ idris-commonmark idris-config idris-lens idris-posix ])
  ];
} ""

And compile it with a simple command:

idris -p effects -p config -p commonmark -p lens -p posix -o bam-idris-blog Main.idr

I plan on using Idris for what it’s good at (i.e. not as a poor Haskell replacement) by introducing dependent types in some way but I’m happy that I was able to improve some Idris libraries and tools.

Please enable JavaScript to view the comments powered by Disqus.