模块与命名空间

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)

修饰符 exportpublic export 说明了哪些名称在其它模块中可见。 之后会详细解释。

这里给出了一个 main 程序(在 bmain.idr 文件中),它利用 Btree 模块对列表排序:

module Main

import Btree

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

同一名称可以在多个模块中定义:名称可以通过模块名来字 限定(Qualified)Btree 模块中定义的全部名称如下:

  • Btree.BTree
  • Btree.Leaf
  • Btree.Node
  • Btree.insert
  • Btree.toList
  • Btree.toTree

如果名称可以区分,就没必要给出完整的限定名。通过明确的限定,或者根据它们的类型, 可以消除名称的歧义。

模块名和文件名之间没有正式的联系,尽管通常会建议使用同一名字。import 语句用于引用文件名,它通过 . 来分隔路径。例如,import foo.bar 会导入文件 foo/bar.idr,其中通常会有模块声明 module foo.bar。对模块名字的唯一要求是, 包含 main 函数的主模块必须命名为 Main,而文件名无需为 Main.idr

导出修饰符

Idris 允许对模块内容的可见性进行细粒度的控制。默认情况下, 模块中定义的所有名称都是私有的。这有助于最小化接口并隐藏内部细节。Idris 允许将函数、类型和接口标记为 privateexportpublic export。 它们的一般含义如下:

  • private 表示完全不被导出。此为默认情况。
  • export 表示顶级类型是导出的。
  • public export 表示整个定义都是导出的。

更改可见性的另一限制是,定义无法引用可见性更低的名称。例如, public export 的定义无法使用私有名称, 而 export 的类型也无法使用私有名称。 这是为了避免私有名称泄露到模块的接口中。

对于函数的意义

  • export 表示导出类型
  • public export 表示导出类型和定义, 导出之后的定义可被使用。 换言之, 定义本身被认为是模块接口的一部分。名字 public export 比较长是为了让你三思而后行。

注解

Idris 中的同义类型可通过编写函数来创建。在为模块设置可见性时, 如果同义类型要在模块外部使用,那么将它们声明为 public export 可能会更好。 否则,Idris 会无法获知该类型与谁同义。

既然 public export 意味着函数的定义是导出的,那么该函数的定义实际上也就成为了模块 API 的一部分。因此,除非你确实想要导出函数的完整定义,否则最好避免将其声明为 public export

对于数据类型的涵义

对于数据类型,其涵义如下:

  • export 的类型构造器是导出的
  • public export 的类型构造器和数据构造器是导出的

对于接口的涵义

对于接口,其涵义如下:

  • export 的接口名字是导出的
  • public export 的接口名、方法名和默认定义都是导出的

%access 指令

默认的导出模式可以通过 %access 指令更改,例如:

module Btree

%access export

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

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))

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

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

在这种情况下,没有访问修饰符的任何函数均可以导出为 export,而不是 private

内部模块 API 的传递

另外,通过对 import 使用 public 修饰符,可将模块内导入的模块再次导出。 例如:

module A

import B
import public C

模块 A 会导出名字 a, 以及模块 C 中所有公共或抽象的名称, 但无法再从模块 B 中导出任何东西。

显式命名空间

在定义模块的同时,也会隐式定义一个命名空间。然而,该命名空间也可以 显式 给出。当你想在同一模块内重载名称时,它会非常有用:

module Foo

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

namespace y
  test : String -> String
  test x = x ++ x

这个(明显人为设计的)模块使用完整的限定名 Foo.x.testFoo.y.test 定义了两个函数,二者可以根据函数类型来消歧义:

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

形参化的块

一组函数的多个参数可通过 parameters 声明进行形参化(Parameterise),例如:

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

parameters 形参块的作用是为块中的每个函数、类型和数据构造器添加形参声明。 具体来说,就是将形参添加到参数列表的前面。在此块外,形参必须显式地给定。 因此在 REPL 中调用 addAll 函数时,它会拥有以下函数声明:

*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,我们必须给出参数 xsy。 在这里,我们可以用占位符来代表类型检查器能推断出的值:

*params> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))
"[1, 2, 3, 4, 5, 6]" : String

提示

形参(Parameter)与实参(Argument)

在数学中,对于函数 f(x)f 为函数名,x 则称作函数 f 的形式参数(Parameter),简称形参;在函数应用时,传输函数的参数则称作实际参数 (Argument),简称实参。例如 f(2) 中的 2 即为传入 f(x) 的实参。

在英文原文中,有时并不明确区分形参与实参,一般统译作「参数」。只有当需要明确区分时, 才分别译作「形参」与「实参」。