Dependent Types Haskell Idris Programming

Idris, a dependent typed functional programming language: install and run on OS X Mavericks

Installing and running Idris programming language on OS X Mavericks. As often in my experience, the package dependency management is rather weak. Fortunately, with a small detour I could work around my issues.

I got rid of the (now deprecated) cabal-dev, updated to the latest version of cabal and thought of installing idris on my machine.  I immediately hit a problem, it won’t install. I get the following error message (log cut down):

$ cabal install idris
Resolving dependencies...
Configuring annotated-wl-pprint-0.5.3...
Building annotated-wl-pprint-0.5.3...
Preprocessing library annotated-wl-pprint-0.5.3...
Registering trifecta-1.5...
Installed trifecta-1.5
cabal: Error: some packages failed to install:
idris- depends on language-java-0.2.6 which failed to install.
language-java-0.2.6 failed during the configure step. The exception was:
ExitFailure 1

So, it’s logical to try and install ‘language-java-0.2.6’. I tried that:

$ cabal install language-java-0.2.6
Resolving dependencies...
Configuring language-java-0.2.6...
cabal: The program 'alex' version >=2.3 is required but it could not be found.
Failed to install language-java-0.2.6
cabal: Error: some packages failed to install:
language-java-0.2.6 failed during the configure step. The exception was:
ExitFailure 1

And that fails too. It turns out I could install the package ‘alex’ manually. So I run this:

$ cabal install alex
Resolving dependencies...
Configuring random-
Building random-
Linking dist/dist-sandbox-c9c9694f/build/alex/alex ...
Installing executable(s) in
Installed alex-3.1.3

That worked. I can now attempt to install Idris:

$ cabal install idris
Resolving dependencies...
Configuring language-java-0.2.6...
Building language-java-0.2.6...
Preprocessing library language-java-0.2.6...
Registering idris-
Installed idris-

Succes. Phew! I am now ready to start using Idris:

$ idris
bash: idris: command not found

Oops! It’s not in the search path, and it’s not obvious where it’s gone. That’s easy, prior to all this I had installed and initialised a cabal sandbox.  So it’s gone in the sandbox, which isn’t in my search path. I went for a sandbox approach because I wanted to isolate my installation of snap and yesod from this Idris playground.

To preserve my sandbox concept, I am going to use an alias to Idris:

$ alias idris="/Volumes/MacintoshHD/usrlocal/bin/.cabal-sandbox/bin/idris"

I typically add such alias to my ~/.bash_profile so that it’s always available.

$ idris
 ____ __ _
 / _/___/ /____(_)____
 / // __ / ___/ / ___/ Version
 _/ // /_/ / / / (__ )
 /___/__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Idris >

And that’s it, I now have Idris available and I can plough on. Ironically, for a language that promises to bring you dependent typed programming, the infrastructure dependency management isn’t stellar. That remains a weak point for me for all things Haskell.

Post Scriptum

  1. This is part of an exploratory journey into dependent types, an exciting concept in computer programming that I wish to use for production code in the near future. To get a glimpse of what this means, read this nice blog post, which, by the way, I think of as a model for introducing advanced programming concepts.
  2. Idris is built on top of Haskell, of which I have a recent version running on my machine. So if you’ve never had any of that kind of stuff on your machine, your mileage might be considerably longer than what I’ve shown here.