Author：Kenta Inoue

This section explains how to install Idris, a functional language that allows writing of dependent types.

Installing Idris

MacOS

• If you have not installed Homebrew, install it.
  • Run the following command in Terminal. Details are available atofficial Homebrew.

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

• We would have been able to install it with brew install idris using Homebrew, but it doesn't seem to be executable now, so We'll install it via Haskell.
• First, we install stack which manages Haskell projects.
  • Run brew update in the terminal.
  • Then run brew install stack.
    • In addition, you can use ghc, a compiler of Haskell.
• Install Idris.
  • Run git clone https://github.com/idris-lang/Idris-dev.git in a terminal.
  • Next, run cd Idris-dev to move to the directory.
  • Then, run stack build.
  • Then, install Idris by stack install.
  • Add the path of idris command.
    • Add the command either ~/.zshrc or ~/.bash_profile (it depends on your shell execution environment) to add PATH.
    • Specifically, In Terminal, run echo 'export PATH=$PATH:~/.local/bin' >> ~/.zshrc or echo 'export PATH=$PATH:~/.local/bin' >> ~/.bash_profile
    • Restart Terminal.
• Check idris command idris can be run.
  • Run idris -version in the restarted terminal.
    • If you see the version information of Idris like 1.3.4-git:xxxxxxxxxxxx, it succeeds.

Windows

we need to download the binary file directly because we can install until stack but not be able to install Idris as the same way of Mac.

• Download the Windows 64-bit version of Idris from github.
• Add the path of idris command.
  • Use Windows PowerShell.
  • Unzip the downloaded file and put it in an appropriate directory.
  • If you unzipped the file to a directory named DIRECTORY, run the following command. setx PATH; DIRECTRY/idris-x.x.x-win64/idris (where x.x.x is the idris version and should be the same name as the actual file name)
    • For example, if you extracted it in download, the DIRECTORY part should be ~/download.
• Restart PowerShell.
• Run idris --version in PowerShell after restart to make sure Idris can be run.

Editor

If you need an editor, the following are available.

If you are not familiar with them, Sakura Editor is enough to write code.

HelloWorld

The Idris file extension is .idr, so the file “xxx.idr” is a Idris program.

For example, you can make a file named "HelloWorld.idr" as follows.

main : IO ()
main = putStrLn "Hello World"

Next, compile this file.

compile

Run idris HelloWorld.idr -o HelloWorld at the directory where the file you want to compile (e.g. HelloWorld.idr) in Terminal. Then an executable file named HelloWorld will be generated. Then, Hello World will be displayed by running ./HelloWorld command. However, in the case of Windows, you may not be able to run the command directly. So, open the idris interactive mode by running idris HelloWorld.idr and run :exec. Then Hello World will be displayed. You will still be in interactive mode, so run :q to quit from there.

Summary

We have described how to install Idris, a pure functional language.