模块和命名空间

一个 Idris 程序由一个模块的集合组成。每个模块包括一个可选的 module 声明，用来给出模块的名称，一个 import 声明列表，给出要导入的其他模块，以及一个类型、接口和函数的声明和定义的集合。例如，下面的列表给出了一个定义二叉树类型的模块 BTree （在文件 BTree.idr 中）：

module BTree

public export
data BTree a = Leaf
             | Node (BTree a) a (BTree a)

export
insert : Ord a => a -> BTree a -> BTree a
insert x Leaf = Node Leaf x Leaf
insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
                                   else (Node l v (insert x r))

export
toList : BTree a -> List a
toList Leaf = []
toList (Node l v r) = BTree.toList l ++ (v :: BTree.toList r)

export
toTree : Ord a => List a -> BTree a
toTree [] = Leaf
toTree (x :: xs) = insert x (toTree xs)

修饰词 export 和 public export 表示哪些名称对其他命名空间可见。这些将在下面进一步解释。

然后，这就给出了一个主程序（在文件 bmain.idr 中），它使用 BTree 模块对一个列表进行排序：

module Main

import BTree

main : IO ()
main = do let t = toTree [1,8,2,7,9,3]
          print (BTree.toList t)

相同的名字可以被定义在多个模块中：名字可以用模块的名字来限定。在 BTree 模块中定义的名字，全限定名如下：

BTree.BTree
BTree.Leaf
BTree.Node
BTree.insert
BTree.toList
BTree.toTree

如果名字没有歧义，就没有必要给出完全限定的名字。名称也可以通过使用 with 关键字给出一个明确的限定，或者根据它们的类型来消除歧义。

with 表达式中的关键字有两种变体：

with BTree.insert (insert x empty) 用于单个名称
with [BTree.insert, BTree.empty] (insert x empty) 用于多个名称

这对于 do 记法特别有用，它通常可以改善错误消息： with MyModule.(>>=) do ...

如果一个文件包含模块声明 module Foo.Bar.MyModule，那么它在 .ipkg 项目文件中 sourcedir`（默认为 `.``）下的相对路径必须为 ./Foo/Bar/MyModule.idr。如果你没有使用 .ipkg 项目文件，则路径必须相对于你运行 Idris 的目录。同理，import 语句也指向去掉扩展名后的相对文件路径，目录之间用点分隔。如上例，所有模块名和目录都必须是首字母大写的标识符。如果文件没有模块声明，则被视为模块 Main。

导出修饰符

Idris 允许对命名空间内容的可见性进行精细的控制。默认情况下，所有定义在名字空间的名字都是私有的。这有助于规范一个最小的接口和隐藏内部细节。Idris 允许函数、类型和接口被标记为 private, export 或 public export 。它们的一般含义如下：

private 意味着它不会被导出。这是默认设置。
export 意味着顶层类型已被导出。
public export 意味着整个定义被导出。

修改可见性的另一个限制是，定义不能引用更低层次的可见性中的任何东西。例如， public export 定义不能使用 private 或 export 名称，而 export 类型不能使用 private 名称。这是为了防止私有名称泄露到模块的接口中。

用于函数时的含义

export 类型被导出
public export 类型和定义被导出，定义被导入后可以使用。换句话说，定义本身被认为是模块接口的一部分。 public export 这个长名字是为了让你在做这件事时三思而行。

备注

Idris 中的类型同义词是通过编写函数创建的。设置模块的可见性时，如果要在模块外使用所有类型的同义词，最好将它们设置为 public export 。否则，Idris 将不知道该同义词是谁的同义词。

由于 public export 意味着一个函数的定义被导出，这实际上使函数定义成为模块 API 的一部分。因此，一般来说，除非你真的想导出完整的定义，否则最好不要对函数使用 public export 。

备注

对于初学者 。如果函数只需要在运行时访问，使用 export 。但是，如果它也要在 编译时使用 （例如，证明一个定理），则使用 public export 。例如，考虑前面讨论的函数 plus : Nat -> Nat -> Nat ，以及下面的定理。 thm : plus Z m = m 。为了证明它，类型检查器需要将 plus Z m 还原为 m （从而得到 thm : m = m ）。* 为了实现这一点，它需要访问*的定义 plus ，其中包括方程式 plus Z m = m 。因此，在这种情况下， plus 必须被标记为 public export 。

数据类型的含义

对于数据类型，其含义是：

export 类型构造器被导出
public export 类型构造器和数据构造器会被导出

接口上的含义

对于接口，其含义是：

export 接口名称被导出
public export 接口名称、方法名称和默认定义被导出

优先级声明的含义

修饰符应用于运算符优先级声明时略有不同。未加修饰的优先级声明会被导出，而不是私有。public export 和 export 没有区别。总结如下：

private 表示优先级声明仅在当前文件内可见。
public export 和 export 等价，都会导出优先级声明。不加修饰符也有同样效果。

传播内部模块的 API

此外，一个模块可以重新输出它所导入的模块，方法是在 public 修改器上使用 import 。例如：

module A

import B
import public C

模块 A 将导出名称 a 以及模块 C 中的任何公共或抽象名称，但不会从模块 B 重新导出任何东西。

重命名导入

有时，能够通过不同的命名空间（通常是较短的命名空间）访问另一个模块中的名称是很方便的。为此，你可以使用 import...as 。例如：

module A

import Data.List as L

这个模块 A 可以访问从模块 Data.List 导出的名称，但也可以通过模块名称 L 明确地访问它们。 import...as 也可以与 import public 结合起来，创建一个模块，从其他子模块导出一个更大的API：

module Books

import public Books.Hardback as Books
import public Books.Comic as Books

在这里，任何导入 Books 的模块都可以访问 Books.Hardback 和 Books.Comic 的导出接口，两者都在命名空间 Books 。

显式命名空间

定义一个模块也隐含地定义了一个命名空间。然而，命名空间也可以被明确地赋予。如果你想在同一个模块中重载名字，这会非常有用：

module Foo

namespace X
  export
  test : Int -> Int
  test x = x * 2

namespace Y
  export
  test : String -> String
  test x = x ++ x

这个模块（公认是设计好的）定义了两个函数，其全称是 Foo.X.test 和 Foo.Y.test ，可以通过其类型来区分：

*Foo> test 3
6 : Int
*Foo> test "foo"
"foofoo" : String

导出规则 public export 和 export ，是 按命名空间 ，而不是 按文件 ，所以上面的两个 test 定义需要 export 标志才能在它们自己的命名空间之外可见。

函数内的显式命名空间

可以在函数的 where 块中显式定义命名空间。与其他定义（如 data 或 record）不同，这类命名空间定义被视为属于该函数定义自身的作用域。

例如，下面的代码可以通过类型检查。

withNSInside : Nat
withNSInside = g where
  namespace X
    export
    g : Nat
    g = 5

useNSFromOutside : Nat
useNSFromOutside = X.g

注意，如果一个包含命名空间定义的函数有参数，则该命名空间内的定义也会拥有这些参数。这是因为这些定义可以访问这些参数的值。

当从函数外部访问带命名空间的定义时，必须显式传递这些参数；而在函数内部访问时则不需要传递。这一行为类似于下文描述的参数化块。请看如下示例。

withNSInside' : String -> Nat
withNSInside' str = String.length g where
  namespace Y
    export
    g : String
    g = str ++ "a"

useNSFromOutside' : String
useNSFromOutside' = Y.g "x" -- value is "xa"

参数化块 - parameters 块

例如，可以使用 parameters 声明，在一些参数上对函数组进行参数化：

parameters (x : Nat) (y : Nat)
  addAll : Nat -> Nat
  addAll z = x + y + z

parameters 块的作用是将声明的参数添加到该块内的每个函数、类型和数据构造器中。具体来说，就是将参数添加到参数列表的前面。在块之外，必须明确地给出参数。 addAll 函数，当从 REPL 中调用时，将有以下类型签名。

*params> :t addAll
addAll : Nat -> Nat -> Nat -> Nat

和以下定义。

addAll : (x : Nat) -> (y : Nat) -> (z : Nat) -> Nat
addAll x y z = x + y + z

参数块可以是嵌套的，也可以包括数据声明，在这种情况下，参数被明确地添加到所有类型和数据构造器中。它们也可以是具有隐含参数的依值类型：

parameters (y : Nat) (xs : Vect x a)
  data Vects : Type -> Type where
    MkVects : Vect y a -> Vects a

  append : Vects a -> Vect (x + y) a
  append (MkVects ys) = xs ++ ys

要在块外使用 Vects 或 append ，我们还必须给出 xs 和 y 的参数。在这里，我们可以使用占位符来表示可以由类型检查器推断出来的值：

Main> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))
"[1, 2, 3, 4, 5, 6]"

你可以用与记录参数相同的语法，指定参数的数量以及是否为隐式参数。

parameters {0 m : Type -> Type} {auto mon : Monad m}