入门

前提需求

在安装 Idris 之前,你需要确认是否拥有所有必须的库和工具。你需要:

  • 近期版本的 GHC 。目前测试过的最早版本为 7.10.3.
  • GNU 多精度运算库 (GMP) 可从 MacPorts/Homebrew 和所有主流 Linux 发行版中获取。

下载并安装

如果你满足所有的前提需求,那么安装 Idris 的最简方式就是在命令行输入:

cabal update; cabal install idris

这会安装 Hackage 中的最新版本及其所有依赖。如果你想要最新开发版的话, 可以在 GitHub 上找到它, 然后根据构建指令来安装。

如果你之前从未安装过使用 Cabal 的东西,Idris 可能不在你的 PATH 中。 如果 Idris 可执行文件无法找到,请将 ~/.cabal/bin 添加到 $PATH 环境变量中。Mac OS X 用户则需要添加 ~/Library/Haskell/bin,Windows 用户通常会发现 Cabal 将程序安装在 %HOME%\AppData\Roaming\cabal\bin 中。

为了检查安装是否成功,你需要编写第一个程序。请创建一个名为 hello.idr 的文件, 其中包含以下文本:

module Main

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

如果你熟悉 Haskell,那会很清楚这段程序在做什么,是如何做的; 如果你对它感到陌生,我们稍后会详细地解释。你可以在命令行中输入 idris hello.idr -o hello 来将程序编译成可执行文件。 这会创建一个名为 hello 的可执行文件,你可以运行它:

$ idris hello.idr -o hello
$ ./hello
Hello world

请注意,美元符号 $ 表示命令行。下面是一些常用的 Idris 命令行选项:

  • -o prog 编译成名为 prog 的可执行文件。
  • --check 无需启动交互式环境就对文件及其依赖进行类型检查。
  • --package pkg 将包添加为依赖,例如通过 --package contrib 来使用 contrib 包。
  • --help 显示用法摘要和命令行选项。

交互式环境

在命令行中输入 idris 来启动交互式环境。你会看到如下内容:

$ idris
    ____    __     _
   /  _/___/ /____(_)____
   / // __  / ___/ / ___/     Version 1.3.1
 _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
/___/\__,_/_/  /_/____/       Type :? for help

Idris>

它会提供一个 ghci 风格的界面,可以像类型检查那样求值表达式、进行定理证明、 编译、编辑、以及执行多种其它操作。命令 :? 会列出所支持的命令。在以下示例中, hello.idr 已被加载,main 的类型已通过检查,之后该程序被编译成了可执行的 hello。 在对某文件类型检查时,如果通过,就会创建它的的字节码版本(本例中为 hello.ibc) 以提升未来的加载速度。在源文件被修改之后,字节码会重新生成。

$ idris hello.idr
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 1.3.1
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Type checking ./hello.idr
*hello> :t main
Main.main : IO ()
*hello> :c hello
*hello> :q
Bye bye
$ ./hello
Hello world