常见问题解答

Idris 项目的目标是什么？

Idris 旨在使软件从业者可以使用与类型相关的高级编程技术。我们遵循的一个重要理念是，Idris 允许软件开发人员表达其数据的不变量并证明程序的属性，但不会要求他们必须这样做。

此常见问题解答中的许多答案都证明了这一理念，我们在做出语言和库设计决策时始终牢记这一点。

Idris 主要是一个研究项目，由圣安德鲁斯大学的 Edwin Brady 领导，并受益于 SICSA (https://www.sicsa.ac.uk) 和 EPSRC (https://www.epsrc.ac.uk) /) 资助。这确实会影响一些设计选择和实现优先级，并且意味着有些事情没有我们想要的那么完美。尽管如此，我们仍在努力使其尽可能广泛地使用！

我在哪里可以找到库？有包管理器吗？

我们还没有包管理器，但您仍然可以在 wiki 上找到库的来源：https://github.com/idris-lang/Idris2/wiki/1-%5BLanguage%5D-Libraries

幸运的是，依赖关系目前并不复杂，但我们仍然希望包管理器提供帮助！目前还没有正式的，但有两个正在开发中：

Inigo: https://github.com/idris-community/inigo
sae: https://github.com/DoctorRyner/sae

Idris 2 可以使用自己进行编译吗？

是的，Idris 2 在 Idris 2 中实现。默认情况下，它以 Chez Scheme 为目标，因此您可以从生成的 Scheme 代码引导，如入门一节所述。

为什么 Idris 2 以 Scheme 为目标？动态类型的目标语言肯定会很慢吗？

您可能会对 Chez Scheme 的速度感到惊讶！ Racket 作为替代目标，也表现良好。两者的性能都优于 Idris 1 后端，后者是用 C 语言编写的，但没有像 Chez 和 Racket 那样经过运行时系统专家数十年的工程努力。 Chez Scheme 还允许我们关闭运行时检查，我们也是这样做的。

作为性能改进的观察性证据，我们使用使用 Chez 运行时构建的编译器版本和使用引导 Idris 2 构建的相同版本，比较了 Idris 2 运行时与 Idris 1 运行时的性能。在戴尔 XPS 13运行 2020 年 5 月 23 日版本的 Ubuntu，性能为：

Idris 2（使用 Chez Scheme 运行时）在 93 秒内检查完自己的源码。
引导 Idris 2（使用 Idris 1 编译）在 125 秒内检查完相同的源码。
Idris 1 在 768 秒内检查完引导 Idris 2 的源码（与上述相同，但由于语法更改而略有不同）。

不幸的是，我们不能用最新版本重复这个实验，因为引导 Idris 2 不再能够构建当前版本。

然而，这并不是一个长期的解决方案，即使它是一种非常方便的引导方式。

Idris 2 可以生成 Javascript 吗？那么可插拔代码生成器呢？

是的！ JavaScript 代码生成器是内置的，可以针对浏览器或 NodeJS。

与 Idris 1 一样，Idris 2 支持可插拔代码生成器允许您为您选择的平台编写后端。

Idris 1 和 Idris 2 之间的主要区别是什么？

最重要的区别是 Idris 2 明确表示擦除类型，因此您可以在编译时看到哪些函数和数据类型参数被擦除，哪些将在运行时出现。您可以在多重性中查看更多详细信息。

Idris 2 具有明显更好的类型检查性能（甚至可能是数量级的差异！）并生成更好的代码。

此外，在 Idris 中实现，我们已经能够利用类型系统来消除一些重要的错误来源！

您可以在自 Idris 1 以来的变化部分中找到更多详细信息。

为什么库中没有更多的线性注解？

理论上，现在 Idris 2 基于定量类型理论（参见章节多重性），我们可以在 Prelude 和 Base 库中编写更精确的类型，从而提供更精确的使用信息。但是，我们选择（暂时）不这样做。例如，考虑一下如果我们这样做会发生什么：

id : (1 _ : a) -> a
id x = x

这绝对是正确的，因为 x 只使用了一次。但是，我们也有:

map : (a -> b) -> List a -> List b

通常情况下，我们不能保证传递给 map 的函数在其参数中是线性的，因此我们不能再说 map id xs ，因为 id 的多重性和传递给 map 的函数的多重性不匹配。

最终，我们希望通过多重性多态来扩展核心语言，这将有助于解决这些问题。在那之前，我们认为线性是类型系统中的一个实验性新特性，因此我们遵循一般理念，即如果你不想使用线性，它的存在一定不会影响你编写程序的方式。

如何在 Idris2 REPL 中获取命令历史记录？

Idris2 REPL 不支持 readline 以保持最小的依赖关系。一个有用的解决方法是安装 rlwrap ，这个程序只需调用 Idris2 repl 作为程序 rlwrap idris2 的参数即可提供命令历史记录。

最终目标是使用 IDE 模式或 Idris API 作为独立于 Idris 2 核心开发的复杂 REPL 实现的基础。据我们所知，目前还没有人致力于此：如果您有兴趣，请联系我们，我们可以帮助您开始！

为什么 Idris 使用及早求值而不是惰性求值？

Idris 使用及早求值来获得更可预测的性能，特别是因为长期目标之一是能够编写高效且经过验证的低级代码，例如设备驱动程序和网络基础设施。此外，Idris 类型系统允许我们准确地声明每个值的类型，从而准确地声明每个值的运行时形式。在惰性语言中，考虑一个类型为 Int 的值：

thing : Int

thing 在运行时的表示形式是什么？它是表示整数的位模式，还是指向某些将计算整数的代码的指针？在 Idris 中，我们决定在类型中使这种区分更加精确：

thing_val : Int
thing_comp : Lazy Int

在这里，从类型中可以清楚地看出， thing_val 被保证是一个具体的 Int ，而 thing_comp 是一个将会产生一个 Int 的计算。

如何创建惰性控制结构？

您可以使用特殊的 Lazy 类型创建控制结构。例如，实现不依赖的 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 类型表示只有在使用它们时才会对这些参数求值，也就是说，它们会被延迟求值。

顺便说一句：我们实际上并没有在 Idris 2 中以这种方式实现 if...then...else...” 相反，它被转换为允许依赖 if 的 case 表达式。

REPL 的求值并不像我预期的那样。这是怎么回事？

作为一种完全依赖类型的语言，Idris 有两个阶段来对事物求值，编译时和运行时。在编译时，它只会求值它知道的全部内容（即终止并覆盖所有可能的输入），以保持类型检查的可判定性。编译时求值器是 Idris 内核的一部分，在 Idris 中作为解释器实现。由于这里的所有内容都具有范式，因此求值策略实际上并不重要，因为无论哪种方式都会得到相同的答案！在实践中，它使用按名称调用，因为这避免了类型检查不需要的子表达式求值。

为方便起见，REPL 使用了编译时的求值概念。除了更容易实现（因为我们有可用的求值器），这对于显示被求值项在类型检查器中如何求值非常有用。所以你可以看到两者之间的区别：

Main> \n, m => S n + m
\n, m => S (plus n m)

Main> \n, m => n + S m
\n, m => plus n (S m)

如果你想在 REPL 编译和执行一个表达式，你可以使用 :exec 命令。在这种情况下，表达式必须具有类型 IO a （ a 可以是任何类型，尽管它不会打印结果）。

为什么我不能使用类型中没有参数的函数？

如果您在以小写字母开头且不应用于任何参数的类型中使用名称，则 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 的类型，而不是其他上下文，就可以清楚地知道隐式绑定的名称是什么。

如果您想在类型中使用未应用的名称，您有三个选项。您可以明确限定它，例如，如果在命名空间 Main 中定义了 ty ，则可以执行以下操作：

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

按照惯例，如果一个名称打算用作类型同义词，最好以大写字母开头以避免这种限制。

最后，您可以使用指令关闭隐式的自动绑定：

%auto_implicits off

在这种情况下，您可以将 n 和 m 绑定为隐式，但不能将 ty 绑定，如下所示：

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

为什么 `Functor` 、 `Applicative` 、 `Monad` 等接口不包含定律？

从表面上看，这听起来是个好主意，因为类型系统允许我们指定规律。不过，我们不会在 prelude 中这样做，主要有两个原因：

它违背了 Idris 允许程序员证明其程序的属性，但不要求它的哲学（在上面）。
在 Idris 系统内，有效、合法的实现不一定是可证明合法的，尤其是在涉及更高阶功能的情况下。

Control.Algebra 中有经过验证的接口版本，它们扩展了带有定律的接口。

我有一个明显终止的程序，但 Idris 说它可能不是完全函数。这是为什么？

由于停机问题的不确定性，Idris 通常无法确定程序是否终止。但是，可以识别某些肯定终止的程序。 Idris 使用 “大小更改终止” 来执行此操作，它查找从函数返回到自身的递归路径。在这样的路径上，必须至少有一个参数收敛到基本情况。

支持相互递归函数
不过，递归路径上的所有函数必须被完整地应用。此外，Idris 不支持高阶应用。
Idris 通过查找对语法上较小的输入参数的递归调用来识别收敛到基本情况的参数。例如 k 在语法上小于 S (S k) 因为 k 是 S (S k) 的子项，但 (k, k) 在语法不小于 (S k, S k) 。

如果你有一个你认为要终止的函数，但 Idris 不这么认为，你可以重新组织程序，或者使用 assert_total 函数。

Idris 有全域多态吗？ `Type` 的类型是什么？

Idris 2 当前实现了 Type : Type 。别担心，这不会永远如此！对于 Idris 1，FAQ 对这个问题的回答如下：

Idris 不是全域多态，而是全域的累积层层级。 Type : Type 1, Type 1 : Type 2 等等。累积性意味着如果 x : Type n 并且 n <= m ，那么 x : Type m `` 。全域级别总是由 Idris 推断，不能明确指定。 REPL 命令 ``:type Type 1 将导致错误，尝试指定任何类型的全域级别也会导致错误。

“Idris”这个名字是什么意思？

到了一定年龄的英国人可能对这条会唱歌的龙比较熟悉。如果这没有帮助，也许你可以发明一个合适的首字母缩略词:-)。

在哪里可以找到 Idris 社区的社区标准？

Idris 社区标准在这里声明