杂项

在本节中，我们将讨论各种附加功能：

自动、隐式和默认参数；
文学编程；和
全域层级。

隐式参数

我们已经看到了隐式参数，它允许在类型检查器 [1] 在可以推断出参数时省略参数，例如。

index : forall a, n . Fin n -> Vect n a -> a

自动隐式参数

在其他情况下，可能不是通过类型检查而是通过在上下文中搜索适当的值或构造证明来推断参数。例如，下面 head 的定义需要证明列表是非空的：

isCons : List a -> Bool
isCons [] = False
isCons (x :: xs) = True

head : (xs : List a) -> (isCons xs = True) -> a
head (x :: xs) _ = x

如果列表静态已知为非空，或者因为它的值是已知的，或者因为上下文中已经存在证明，则可以自动构造证明。自动隐式参数允许这种情况静默发生。我们定义 head 如下：

head : (xs : List a) -> {auto p : isCons xs = True} -> a
head (x :: xs) = x

隐式参数上的 auto 注解意味着 Idris 将尝试通过搜索适当类型的值来填充隐式参数。事实上，在内部，这正是接口解析的工作方式。它将按顺序尝试以下操作：

局部变量，即模式匹配或 let 绑定中的名称，具有完全正确的类型。
所需类型的构造函数。如果它们有参数，它将递归搜索的最大深度为 100。
具有函数类型的局部变量，递归搜索参数。
任何具有适当返回类型且标有 %hint 注解的函数。

在没有找到证明的情况下，可以像往常一样明确提供：

head xs {p = ?headProof}

默认隐式参数

除了让 Idris 自动查找给定类型的值之外，有时我们还希望有一个具有特定默认值的隐式参数。在 Idris 中，我们可以使用 default 注解来做到这一点。虽然这主要是为了帮助自动构建 auto 失败或发现无用值的证明，但首先考虑不涉及证明的更简单的情况可能更容易。

如果我们想计算第 n 个斐波那契数（并将第 0 个斐波那契数定义为 0），我们可以这样写：

fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
fibonacci {lag} Z = lag
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n

在这个定义之后， fibonacci 5 等价于 fibonacci {lag=0} {lead=1} 5 ，并且会返回第 5 个斐波那契数。请注意，虽然这有效，但这不是 default 注解的预期用途。此处仅用于说明目的。通常， default 用于提供自定义证明搜索脚本之类的东西。

文学编程

与 Haskell 一样，Idris 支持文学编程。如果一个文件的扩展名为 .lidr ，那么它被认为是一个文学(literate) 文件。在文学编程中，所有内容都被假定为注释，除非该行以大于号 > 开头，例如：

> module literate

This is a comment. The main program is below

> main : IO ()
> main = putStrLn "Hello literate world!\n"

另一个限制是程序行（以 > 开头）和注释行（以任何其他字符开头）之间必须有一个空行。

累积性

警告

尚未在 IDRIS 2 中

由于值可以出现在类型中，然后 反之亦然 ，因此类型本身具有类型是很自然的。例如：

*universe> :t Nat
Nat : Type
*universe> :t Vect
Vect : Nat -> Type -> Type

但是 Type 的类型呢？如果我们问 Idris ，它会报告：

*universe> :t Type
Type : Type 1

如果 Type 是它自己的类型，那么它会因为 Girard 悖论而导致不一致性，所以内部有一个层级类型（或全域）：

Type : Type 1 : Type 2 : Type 3 : ...

全域是 累积的 ，也就是说，如果 x : Type n 我们也可以拥有 x : Type m ，只要 n < m 。如果发现任何不一致，类型检查器会生成这样的全域约束并报告错误。通常，程序员不需要担心这一点，但它确实会防止（构造出）以下程序：

myid : (a : Type) -> a -> a
myid _ x = x

idid :  (a : Type) -> a -> a
idid = myid _ myid

myid 对自身的应用会导致 Universe 层次结构中的循环 - myid 的第一个参数是 Type ，如果应用它，那么其级别不能低于所要求的级别。