常见问题解答(FAQ)¶
Agda 跟 Idris 有啥不一样啊?¶
和 Idris 一样,Agda 也是个带有依赖类型的函数式语言,并且支持依赖模式匹配。
它们都能编写程序和证明。不过,Idris 一开始就侧重于为通用编程而设计,而非 Agda
侧重的定理证明。因此,它支持与系统库和 C 程序的互操作性,以及用于实现 EDSL
(领域特定语言)的语言构造。它还包括更高级的编程构造,例如接口(类似于类型类)和
do
记法。
Idris 支持多种后端(默认为 C 和 JavaScript,可以通过插件添加更多),拥有一个 C 编写的,带有垃圾收集器和内建并发消息传递的参考运行时系统。
有标准库文档没?有函数列表没?¶
预置包的 API 文档已在文档页中列出。
不幸的是,Idris 的默认前导和预置包在文档方面未必完整。其它查找函数的方式包括:
- REPL 命令:
- 使用 :apropos 来搜索文档和函数名中的文本。
- 使用 :search 来根据类型搜索函数。
- 使用 :browse 来列出给定名字空间中的内容。
- 使用 REPL 的自动补全功能。
- 使用 grep 在 libs/ 中搜索源码
如果你发现预置包缺少文档,请随心为它补充一些。当然也可以通知别人来做这件事。 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
t
和 e
的类型 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
这里的 n
、m
和 ty
是隐式绑定的。此规则同样适用于在别处定义的,
带这类名字的函数。例如,你或许还有:
ty : Type
ty = String
即便如此,ty
还是会被视作 append
定义中隐式绑定的参数,而不会让 append
的类型等价于你预想的:
append : Vect n String -> Vect m String -> Vect (n + m) String
采用了此规则后,你无需其它上下文,只要查看 append
的类型就能明白哪些是隐式绑定的名字。
如果你想在类型中使用不被应用的名字,那么有两种选择:你可以显式地限定它,例如,
若 ty
在 Main
的命名空间中定义,你可以这样做:
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)
,因为k
是S (S k)
的子项(subterm), 然而(k, k)
在语法上却不小于(S k, S k)
。
如果你有个确信会终止的函数,但 Idris 不信,那么你可以调整程序的结构,或者使用
assert_total
函数。
<<<<<<< HEAD Idris 啥时候能自举啊? ======================
这事不急,虽说从长远来看这主意不错。就目前来说,实现支持自举的库是一项很有价值的工作, 比如说参数解析器以及符合 POSIX 标准的库用于系统交互。
Idris 有全域多态不? Type
是啥类型的?¶
Idris 并没有全域多态(Universe Polymorphism),而是拥有全域的积累层级
(Cumulative Hierarchy),如 Type : Type 1
、Type 1 : Type 2
等等。
积累性的意思是,若 x : Type n
且 n <= m
,则 x : Type m
。
全域的级别总是由 Idris 推导,且无法被显式地指定。执行 REPL 命令 :type Type 1
以及试图为任何类型指定全域级别时,都会产生一个错误。
为啥 Idris 用 Double
不用 Float64
?¶
历史上 C 和很多语言都用分别用 Float
和 Double
来表示 32 位和
64 位的浮点数。较新的语言,如 Rust 和 Julia 都开始遵循 IEEE 浮点运算标准
(IEEE 754) 的命名规范了。
它将单精度和双精度的数描述为 Float32
和 Float64
,其大小在类型名中描述。
由于开发者更熟悉旧有的命名约定,而 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 对此 推送请求 的回应。