常见问题解答(FAQ)

Agda 跟 Idris 有啥不一样啊?

和 Idris 一样,Agda 也是个带有依赖类型的函数式语言,并且支持依赖模式匹配。 它们都能编写程序和证明。不过,Idris 一开始就侧重于为通用编程而设计,而非 Agda 侧重的定理证明。因此,它支持与系统库和 C 程序的互操作性,以及用于实现 EDSL (领域特定语言)的语言构造。它还包括更高级的编程构造,例如接口(类似于类型类)和 do 记法。

Idris 支持多种后端(默认为 C 和 JavaScript,可以通过插件添加更多),拥有一个 C 编写的,带有垃圾收集器和内建并发消息传递的参考运行时系统。

有标准库文档没?有函数列表没?

预置包的 API 文档已在文档页中列出。

不幸的是,Idris 的默认前导和预置包在文档方面未必完整。其它查找函数的方式包括:

  • REPL 命令:
    • 使用 :apropos 来搜索文档和函数名中的文本。
    • 使用 :search 来根据类型搜索函数。
    • 使用 :browse 来列出给定名字空间中的内容。
  • 使用 REPL 的自动补全功能。
  • 使用 greplibs/ 中搜索源码

如果你发现预置包缺少文档,请随心为它补充一些。当然也可以通知别人来做这件事。 Idris 提供了显示富文档的语法,富文档可使用 :doc 命令浏览,并在生成的 HTML API 文档中列出。

Idris 能拿来干活不?

Idris 主要是个研究工具,用来探索用依赖类型开发软件的可能性,也就是说它的主要目的(还) 不是开发可用于生产的系统。因此,某些方面上它还有些粗糙,也缺少很多库。现在还没人全职搞 Idris,我们目前也没有资源来独立完善该系统。因此,我们不推荐你围绕它来开展业务!

话虽如此,我们非常欢迎帮助推进 Idris 适应生产的贡献,包括(但不限于)额外的库支持、 完善运行时系统(并确保其健壮性)、提供并维护 JVM 后端等等。

为啥 Idris 用了及早求值,不用惰性求值啊?

Idris 采用及早求值主要是为了能更好地预测性能,特别是其长期目标之一就是能够编写高效 且经过验证的底层代码,例如设备驱动以及网络设施。此外,Idris 的类型系统能让我们精确地 指明每个值的类型,因此也就能确定每个值在运行时的形式。在惰性求值的语言中,考虑一个 Int 类型的值:

thing : Int

thing 在运行时是如何表示的?它是一个按照位模式来表示的整数, 还一个是指向了能计算出整数的代码的指针?在 Idris 中,我们决定按照类型来精确地区分它们:

thing_val : Int
thing_comp : Lazy Int

这样,thing_val 就能确保为具体的 Int,而 thing_comp 则是会产生 Int 的计算。

俺咋弄个惰性控制结构呐?

你可以用特殊的 Lazy 类型来创建这种控制结构。例如,Idris 中的 if...then...else... 会被扩展为 ifThenElse 函数的应用。 它在库中对布尔值的默认实现如下:

ifThenElse : Bool -> (t : Lazy a) -> (e : Lazy a) -> a
ifThenElse True  t e = t
ifThenElse False t e = e

te 的类型 Lazy a 指出它们只会在需要时被求值,也就是说,它们是惰性求值的。

REPL 里头的求值行为跟咱想的不一样啊,这咋回事儿= =?

作为一个完全依赖类型的语言,Idris 的求值分为两个阶段,编译时与运行时。在编译时, 它只会对已知完全(即保证会终止且覆盖了所有可能输入)的东西求值, 以此来保持类型检查的可判定性。编译时的求值器属于 Idris 核心的一部分,它用 Haskell 编写,按照值的 HOAS(Higher Order Abstract Syntax 高阶抽象语法)风格的表示来实现。 由于已知所有东西都有规范的形式,选用哪种求值策略实际上也就无关紧要了, 因为它们都会得到相同的答案,而在实践中,它会执行 Haskell 运行时系统选择的任何事情。

按照约定,REPL 使用编译时求值的概念。除了更容易实现外(因为我们可以用求值器), 它在展示项(Term)如何在类型检查器中求值时也非常有用。

Idris> \n, m => (S n) + m
\n => \m => S (plus n m) : Nat -> Nat -> Nat

Idris> \n, m => n + (S m)
\n => \m => plus n (S m) : Nat -> Nat -> Nat

为啥咱不能在类型里用没参数的函数呐?

如果你在类型中使用小写字母开头的名字,且它们没用被应用于任何参数,那么 Idris 会把它视为隐式绑定的参数。例如:

append : Vect n ty -> Vect m ty -> Vect (n + m) ty

这里的 nmty 是隐式绑定的。此规则同样适用于在别处定义的, 带这类名字的函数。例如,你或许还有:

ty : Type
ty = String

即便如此,ty 还是会被视作 append 定义中隐式绑定的参数,而不会让 append 的类型等价于你预想的:

append : Vect n String -> Vect m String -> Vect (n + m) String

采用了此规则后,你无需其它上下文,只要查看 append 的类型就能明白哪些是隐式绑定的名字。

如果你想在类型中使用不被应用的名字,那么有两种选择:你可以显式地限定它,例如, 若 tyMain 的命名空间中定义,你可以这样做:

append : Vect n Main.ty -> Vect m Main.ty -> Vect (n + m) Main.ty

此外,你还可以使用不以小写字母开头的名字,它决不会被隐式绑定:

Ty : Type
Ty = String

append : Vect n Ty -> Vect m Ty -> Vect (n + m) Ty

按照约定,如果你打算将一个名字用作类型同义,那么最好以大写字母开头来避免此限制。

这破程序明显能停,为啥 Idris 还说它有可能不完全?

由于停机问题的不可判定性, Idris 通常无法判定一个程序是否会停止。然而,我们可以找出某些确定可以终止的程序。 Idris 使用「大小改变终止(size change termination)」来寻找从函数返回到自身的递归路径。 在此路径上,至少必有一个参数会收敛到基本情况。

  • Idris 支持相互递归的函数
  • 不过,递归路径上的所有函数必须被完整地应用。此外,Idris 不支持高阶应用。
  • 在递归调用的过程中,Idris 会查找语法上更小的输入参数,以此来识别能收敛到基本情况的参数。 例如,k 在语法上小于 S (S k),因为 kS (S k) 的子项(subterm), 然而 (k, k) 在语法上却不小于 (S k, S k)

如果你有个确信会终止的函数,但 Idris 不信,那么你可以调整程序的结构,或者使用 assert_total 函数。

<<<<<<< HEAD Idris 啥时候能自举啊? ======================

这事不急,虽说从长远来看这主意不错。就目前来说,实现支持自举的库是一项很有价值的工作, 比如说参数解析器以及符合 POSIX 标准的库用于系统交互。

Idris 有全域多态不? Type 是啥类型的?

Idris 并没有全域多态(Universe Polymorphism),而是拥有全域的积累层级 (Cumulative Hierarchy),如 Type : Type 1Type 1 : Type 2 等等。 积累性的意思是,若 x : Type nn <= m,则 x : Type m。 全域的级别总是由 Idris 推导,且无法被显式地指定。执行 REPL 命令 :type Type 1 以及试图为任何类型指定全域级别时,都会产生一个错误。

为啥 Idris 用 Double 不用 Float64

历史上 C 和很多语言都用分别用 FloatDouble 来表示 32 位和 64 位的浮点数。较新的语言,如 Rust 和 Julia 都开始遵循 IEEE 浮点运算标准 (IEEE 754) 的命名规范了。 它将单精度和双精度的数描述为 Float32Float64,其大小在类型名中描述。

由于开发者更熟悉旧有的命名约定,而 Idris 的开发者也选择了它,因此 Idris 采用了 C 风格的约定。也就是说名称 Double 用于描述双精度浮点数,而 Idris 现在还不支持 32 位浮点数。

-ffreestanding 是啥?

在相对路径中拥有自己的库和编译器时,可使用 freestanding 命令行参数来构建 Idris 二进制文件。当构建过程中的安装目录未知时,它对于构建二进制文件来说非常有用。 当传入此参数时,IDRIS_LIB_DIR 环境变量需要设置为相对与 idris 可执行文件所在的 Idris 库的路径。 IDRIS_TOOLCHAIN_DIR 环境变量是可选的,如果设置了它,Idris 就会在该路径下寻找 C 编译器。例如:

IDRIS_LIB_DIR="./libs" \
IDRIS_TOOLCHAIN_DIR="./mingw/bin" \
CABALFLAGS="-fffi -ffreestanding -frelease" \
make

话说「Idris」是个啥名儿 O_O?

有一定年龄的英国人可能很熟悉唱歌贼好听的小火龙妹砸。 你要是不满意,自己想个好词儿啊(手动微笑 :-)

还能有 Unicode 操作符不?

下面是为什么我们不应该支持 Unicode 操作符的原因:

  • 它难以输入(如果你在使用别人的代码,这点就很重要)。很多编辑器都有它自己的输入法, 不过你必须知道怎么输入。
  • 并不是任何软件都能轻松支持它。在一些移动 Email 客户端、基于终端的 IRC 客户端、 以及 Web 浏览器等软件中都会出现渲染问题。
  • 即便我们不在标准库中使用它(绝对不会!),然而只要有人在他们的库代码中用了它, 别人就得去处理它。
  • 有太多字符看起来太像了。单是分不清 0 和 O 就会造成很多麻烦,更不说各式各样的冒号和括号了。

如果使用得当,Unicode 操作符能让代码看起来更漂亮,然而 lhs2TeX 也能。 也许几年后情况有变,软件能更好地应对它,到时候重新审视它才有意义。然而目前, Idris 不会为操作符提供任何 Unicode 符号。

这似乎是个 Wadler 定律 在工作中的实例。

本答案基于 Edwin Brady 对此 推送请求 的回应。

Idris 有社区准则不?

这里 是Idris 社区规范的声明。

还有哪儿能找到解答啊?

Github 的维基上还有个非官方 FAQ, 其中解答了更多技术问题,而且经常更新。