Idris 语言文档 Version 1.3.1

I d r i s 语 语 语言 言 言文 文 文档 档 档 Ve r s io n 1 .3 .1 C o n t e n t s 1 I d r i s 教 教 教程 程 程 2 2 常 常 常见 见 见问 问 问题 题 题解 解 解答 答 答（ （ （F A Q ） ） ） 64 3 用 用 用 I d r i s 实 实 实现 现 现带 带 带有 有 有状 状 状态 态 态的 的 的系 系 系统 统 统： ： ：S T 教 教 教程 程 程 69 4 Th e E ff e c t s Tu t or i al 102 5 Th e or e m P r ov i n g 136 6 L an gu age R e f e r e n c e 147 7 Tu t or i al s on t h e I d r i s L an gu age 215 注 注 注解 解 解: 奉 奤 奲 奩 女 文档已按照 创 创 创作 作 作共 共 共用 用 用 C C 0 许 许 许可 可 可协 协 协议 议 议 发布。因此根据法律规定， I d r i s 社 社 社区 区 区 已放弃对 奉 奤 奲 奩 女 文档的所有版权以及相关或邻接的权利。 关于 奃 奃 夰 的更多信息参见：奨 奴 奴 奰 女 夺 夯夯奣 奲 奥 奡奴 奩 奶 奥 奣 奯奭 奭 奯奮 女 央 奯奲 奧夯奰 奵 奢 奬 奩 奣 奤 奯奭 奡奩 奮 夯奺 奥 奲 奯夯失央 夰夯奤 奥 奥 奤 央 奺 奨 失 C H AP T E R 1 I d r i s 教程 本文档为 奉 奤 奲 奩 女 的教程，它简单介绍了如何用 奉 奤 奲 奩 女 语言编程。 文档中覆盖了该语言的核心特性，并假 定你至少熟悉一门函数式编程语言，如 奈奡女 奫 奥 奬 奬 或 奏 奃 奡奭 奬 。 注 注 注解 解 解: 奉 奤 奲 奩 女 文档已按照 创 创 创作 作 作共 共 共用 用 用 C C 0 许 许 许可 可 可协 协 协议 议 议 发布。因此根据法律规定， I d r i s 社 社 社区 区 区 已放弃对 奉 奤 奲 奩 女 文档的所有版权以及相关或邻接的权利。 关于 奃 奃 夰 的更多信息参见：奨 奴 奴 奰 女 夺 夯夯奣 奲 奥 奡奴 奩 奶 奥 奣 奯奭 奭 奯奮 女 央 奯奲 奧夯奰 奵 奢 奬 奩 奣 奤 奯奭 奡奩 奮 夯奺 奥 奲 奯夯失央 夰夯奤 奥 奥 奤 央 奺 奨 1. 1 引 引 引言 言 言 在传统编程语言中，类 类 类型 型 型 与 值 值 值 之间有明确的区分。例如在 奈奡女 奫 奥 奬 奬 中夬 下面这些类型分别表示整数、 字符、字符列表 以及任意值的列表： • Int夬 Char夬 [Char]夬 [a] 与此对应，下面这些值分别为上述类型的成员： • 42夬 ’a’夬 "Hello world!"夬 [2,3,4,5,6] 然而，在带有 依 依 依赖 赖 赖类 类 类型 型 型（ （ （D e p e n d e n t Ty p e ） ） ） 的语言中，它们的区别并不明显。 依赖类型允许类型 「依赖」于值，换句话说，类型是 一 一 一等 等 等（ （ （F i r s t - C l as s ） ） ） 的语言构造， 即它可以像值一样进行操作。 标准范例就是带长度的列表类型1 Vect n a， 其中 a 为元素的类型，而 n 为该列表的长度且可以任意 长。 当类型包含了描述其性质的值（如列表的长度）时，它就能描述函数自身的性质了。 比如连接两个列 表的操作，它拥有性质：结果列表的长度为两个输入列表的长度之和。 因此我们可以为 app 函数赋予 如下类型，它用于连接向量（奖奥 奣 奴 奯奲 ）： app : Vect n a -> Vect m a -> Vect (n + m) a 1 也许会令人困惑，它在依赖类型编程的文献中通常被称作「向量 ( V e c t o r ) 」。 夲 I d r i s 语 语 语言 言 言文 文 文档 档 档, 版 版 版本 本 本 1. 3. 1 本教程介绍了 奉 奤 奲 奩 女 ，一个通用的依赖类型函数式编程语言。奉 奤 奲 奩 女 项目旨在为可验证的通用编程打造一 个依赖类型的语言。 为此，奉 奤 奲 奩 女 被设计成了编译型语言，目的在于生成高效的可执行代码。 它还拥有 轻量的外部函数接口，可与外部 C 库轻松交互。 1. 1. 1 目 目 目标 标 标受 受 受众 众 众 本教程面向已经熟悉函数式语言（如 奈奡女 奫 奥 奬 奬 或 奏 奃 奡奭 奬 ）的读者，旨在简要地介绍该语言。 尽管大多 数概念都会有简单的解释，读者仍须熟悉 奈奡女 奫 奥 奬 奬 的语法。 我们亦假设读者有兴趣使用依赖类型来编写 和验证系统软件。 对 奉 奤 奲 奩 女 更加深入的介绍，见 奅 奤 奷 奩 奮 奂 奲 奡奤 她 所著的《 奉 奤 奲 奩 女 类型驱动开发 》， 其进度要慢得多，涵盖了 交互式程序开发以及更多的例子。本书可从 奍 奡奮 奮 奩 奮 奧 获取。 1. 1. 2 示 示 示例 例 例代 代 代码 码 码 本教程中的示例代码通过了 奉 奤 奲 奩 女 的测试。这些文件可在 奉 奤 奲 奩 女 发行版的 samples 目录中找到，因此您 可以轻松使用它们。然而，我们强烈建议您不要只是载入后阅读， 而是亲自输入它们。 1. 2 入 入 入门 门 门 1. 2. 1 前 前 前提 提 提需 需 需求 求 求 在安装 奉 奤 奲 奩 女 之前，你需要确认是否拥有所有必须的库和工具。你需要： • 近期版本的 奇 奈奃 。目前测试过的最早版本为 夷央 失夰央 夳央 • G NU 多 多 多精 精 精度 度 度运 运 运算 算 算库 库 库 夨 奇 奍 奐 天 可从 奍 奡奣 奐 奯奲 奴 女 夯奈奯奭 奥 奢 奲 奥 奷 和所有主流 奌奩 奮 奵 奸 发行版中获取。 1. 2. 2 下 下 下载 载 载并 并 并安 安 安装 装 装 如果你满足所有的前提需求，那么安装 奉 奤 奲 奩 女 的最简方式就是在命令行输入： cabal update; cabal install idris 这会安装 奈奡奣 奫 奡奧奥 中的最新版本及其所有依赖。如果你想要最新开发版的话， 可以在 奇 奩 奴 奈奵 奢 上找到 它， 然后根据构建指令来安装。 如果你之前从未安装过使用 奃 奡奢 奡奬 的东西，奉 奤 奲 奩 女 可能不在你的 奐 奁奔 奈 中。 如果 奉 奤 奲 奩 女 可执行文件 无法找到，请将 ~/.cabal/bin 添加到 $PATH 环境变量中。奍 奡奣 奏 奓 奘 用户则需要添加 ~/Library/ Haskell/bin，套 奩 奮 奤 奯奷 女 用户通常会发现 奃 奡奢 奡奬 将程序安装在 %HOME%\AppData\Roaming\cabal\bin 中。 为了检查安装是否成功，你需要编写第一个程序。请创建一个名为 hello.idr 的文件， 其中包含以下 文本： module Main main : IO () main = putStrLn "Hello world" 1. 2. 入 入 入门 门 门 3 I d r i s 语 语 语言 言 言文 文 文档 档 档, 版 版 版本 本 本 1. 3. 1 如果你熟悉 奈奡女 奫 奥 奬 奬 ，那会很清楚这段程序在做什么，是如何做的； 如果你对它感到陌生，我们稍后会 详细地解释。你可以在命令行中输入 idris hello.idr -o hello 来将程序编译成可执行文件。 这会 创建一个名为 hello 的可执行文件，你可以运行它： $ idris hello.idr -o hello $ ./hello Hello world 请注意，美元符号 $ 表示命令行。下面是一些常用的 奉 奤 奲 奩 女 命令行选项： • -o prog 编译成名为 prog 的可执行文件。 • --check 无需启动交互式环境就对文件及其依赖进行类型检查。 • --package pkg 将包添加为依赖，例如通过 --package contrib 来使用 奣 奯奮 奴 奲 奩 奢 包。 • --help 显示用法摘要和命令行选项。 1. 2. 3 交 交 交互 互 互式 式 式环 环 环境 境 境 在命令行中输入 idris 来启动交互式环境。你会看到如下内容： $ idris ____ __ _ / _/___/ /____(_)____ / // __ / ___/ / ___/ Version 1.3.1 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help Idris> 它会提供一个 ghci 风格的界面，可以像类型检查那样求值表达式、进行定理证明、 编译、编辑、以及 执行多种其它操作。命令 :? 会列出所支持的命令。在以下示例中， hello.idr 已被加载，main 的类 型已通过检查，之后该程序被编译成了可执行的 hello。 在对某文件类型检查时，如果通过，就会创建 它的的字节码版本（本例中为 hello.ibc） 以提升未来的加载速度。在源文件被修改之后，字节码会 重新生成。 $ idris hello.idr ____ __ _ / _/___/ /____(_)____ / // __ / ___/ / ___/ Version 1.3.1 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help Type checking ./hello.idr *hello> :t main Main.main : IO () *hello> :c hello *hello> :q Bye bye $ ./hello Hello world 1. 3 类 类 类型 型 型与 与 与函 函 函数 数 数 1. 3. 类 类 类型 型 型与 与 与函 函 函数 数 数 4 I d r i s 语 语 语言 言 言文 文 文档 档 档, 版 版 版本 本 本 1. 3. 1 1. 3. 1 原 原 原语 语 语类 类 类型 型 型 奉 奤 奲 奩 女 定义了一些原语（奐 奲 奩 奭 奩 奴 奩 奶 奥 ）类型：Int、Integer 和 Double 用于数值类型， Char 和 String 用 于文本操作，Ptr 则表示外部指针。库中还声明了一些数据类型， 包括 Bool 及其值 True 和 False。 我们可以用这些类型来声明常量。 将以下内容保存到文件 Prims.idr 中，在命令行中输入 idris Prims.idr 以将其加载到 奉 奤 奲 奩 女 的交互式环境中： module Prims x : Int x = 42 foo : String foo = "Sausage machine" bar : Char bar = 'Z' quux : Bool quux = False 提 提 提示 示 示: 原语（奐 奲 奩 奭 奩 奴 奩 奶 奥 ）本意为不可分割的基本构件，原语类型即最基本的类型。 奉 奤 奲 奩 女 文件由一个可选的模块声明（此处为 module Prims），一个可选的导入列表， 一组声明及其定义 构成。在本例中并未指定导入。奉 奤 奲 奩 女 可由多个模块构成， 每个模块中的每个定义都有它自己的命名空 间。这点会在 模块与命名空间 夨 姩 妡妵 夲夹天 一节中进一步讨论。在编写 奉 奤 奲 奩 女 程序时，声明的顺序和缩进都 很重要。 函数和数据类型必须先定义再使用，每个定义都必须有类型声明，例如之前列出的 x : Int 和 foo : String。新声明的缩进级别必须与之前的声明相同。 此外，分号 ; 也可用于结束声明。 库模块 Prelude 会在每个 奉 奤 奲 奩 女 程序中自动导入，包括 奉 奏 功能，算术运算， 数据结构以及多种通用函 数。奐 奲 奥 奬 奵 奤 奥 中定义了一些算术和比较运算符， 我们可以在提示符中使用它们。在提示符中进行求值会 给出一个答案及其类型。例如： *prims> 6*6+6 42 : Integer *prims> x == 6*6+6 True : Bool 奉 奤 奲 奩 女 为原语类型定义了所有的普通算术和比较运算。它们通过接口进行了重载， 并可被扩展以适用于 用户定义的类型，这点我们会在 接口 夨 姩 妡妵 夲失天 一节中讨论。布尔表达式可通过 if...then...else 构 造来测试，例如： *prims> if x == 6 * 6 + 6 then "The answer!" else "Not the answer" "The answer!" : String 1. 3. 2 数 数 数据 据 据类 类 类型 型 型 数据类型的声明方式和语法与 奈奡女 奫 奥 奬 奬 非常相似。例如，自然数和列表的声明如下： data Nat = Z | S Nat -- 自然数（零与后继） data List a = Nil | (::) a (List a) -- 多态列表 以上声明来自于标准库。一进制自然数要么为零（Z）， 要么就是另一个自然数的后继（S k）；列表 要么为空（Nil）， 要么就是一个值被添加在另一个列表之前（x :: xs）。 在 List 的声明中，我们 使用了中缀操作符 ::。 像这样的新操作符可通过缀序声明（奆 奩 奸 奩 奴 她 奄 奥 奣 奬 奡奲 奡奴 奩 奯奮 ）来添加，如下所示： 1. 3. 类 类 类型 型 型与 与 与函 函 函数 数 数 5 I d r i s 语 语 语言 言 言文 文 文档 档 档, 版 版 版本 本 本 1. 3. 1 infixr 10 :: 函数、数据构造器与类型构造器均可用名字作为中缀操作符。它们被括在括号中时， 也可作为前缀形 式使用，例如 (::)。中缀操作符可使用下面的任何符号： :+-*\/=.?|&><!@$%^~# 有 些 以 这 些 符 号 构 成 的 操 作 符 无 法 被 用 户 定 义 。 它 们 是 :、=>、->、<-、=、?=、|、**、 ==>、\、%、~、? 以及 !。 1. 3. 3 函 函 函数 数 数 函数通过模式匹配（奐 奡奴 奴 奥 奲 奮 奍 奡奴 奣 奨 奩 奮 奧）实现，语法同样和 奈奡女 奫 奥 奬 奬 类似。 其主要的不同在于 奉 奤 奲 奩 女 的 所有函数都需要类型声明，声明中使用单冒号 : （而非 奈奡女 奫 奥 奬 奬 的双冒号 :: ）。自然数的某些运算函 数定义如下，同样来自标准库： -- 一进制加法 plus : Nat -> Nat -> Nat plus Z y = y plus (S k) y = S (plus k y) -- 一进制乘法 mult : Nat -> Nat -> Nat mult Z y = Z mult (S k) y = plus y (mult k y) 标准算术运算符 + 和 * 同样根据 Nat 的需要进行了重载， 它们使用上面的函数来定义。和 奈奡女 奫 奥 奬 奬 不同的是，类型和函数名的首字母并无大小写限制。 函数名（前面的 plus 和 mult ），数据构造器 （Z、S、Nil 和 ::） 以及类型构造器（Nat 和 List）均属同一命名空间。不过按照约定， 数据类型和 构造器的名字通常以大写字母开头。我们可以在 奉 奤 奲 奩 女 提示符中测试这些函数： Idris> plus (S (S Z)) (S (S Z)) 4 : Nat Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z))) 12 : Nat 注 注 注解 解 解: 在显示一个 Nat 元素，如 (S (S (S (S Z)))) 时，奉 奤 奲 奩 女 会将其显示为 4。 plus (S (S Z)) (S (S Z)) 的结果实际上为 (S (S (S (S Z))))， 即自然数 4。这点可在 奉 奤 奲 奩 女 提示符中验证： Idris> (S (S (S (S Z)))) 4 : Nat 和算术运算符一样，整数字面也可通过接口重载，因此我们也能像下面这样测试函数： Idris> plus 2 2 4 : Nat Idris> mult 3 (plus 2 2) 12 : Nat 你可能会很好奇，既然计算机已经完美内建了整数运算，我们为何还需要一进制的自然数？ 主要的原 因在于一进制数的结构非常便于推理，而且易与其它数据结构建立联系， 我们之后就会看到。尽管如 此，我们并不希望以牺牲效率为代价获得这种便捷。幸运的是， 奉 奤 奲 奩 女 知道 Nat （以及类似的结构化类 型）和数之间的联系， 这意味着 奉 奤 奲 奩 女 可以优化它们的表示以及像 plus 和 mult 这样的函数。 1. 3. 类 类 类型 型 型与 与 与函 函 函数 数 数 6 I d r i s 语 语 语言 言 言文 文 文档 档 档, 版 版 版本 本 本 1. 3. 1 where 从 从 从句 句 句 函数也可通过 where 从句来 局 局 局部 部 部 地定义。例如，要定义用来反转列表的函数， 我们可以使用辅助函数 来累加新的，反转后的列表，并且它无需全局可见： reverse : List a -> List a reverse xs = revAcc [] xs where revAcc : List a -> List a -> List a revAcc acc [] = acc revAcc acc (x :: xs) = revAcc (x :: acc) xs 缩进是十分重要的，where 块中函数的缩进层次必须比外层函数更深。 注 注 注解 解 解: 作用域 任何外层作用域中可见，且没有被重新被定义过的名字，在 where 从句中也可见 （这里的 xs 被重新定 义了）。若某个名字是某个类型的 形 形 形参 参 参（ （ （P ar am e t e r ） ） ），那么仅当它在类型中出现时才会在 where 从 句的作用域中，即，它在整体结构中是固定不变的。 除函数外，where 块中也可包含局部数据声明，以下代码中的的 MyLT 就无法在 foo 的定义之外访问。 foo : Int -> Int foo x = case isLT of Yes => x*2 No => x*4 where data MyLT = Yes | No isLT : MyLT isLT = if x < 20 then Yes else No 通常，where 从句中定义的函数和其它顶层函数一样，都需要类型声明。 然而，函数 f 的类型声明可 在以下情况中省略： • f 出现在顶层定义的右边 • f 的类型完全可以通过其首次应用来确定 因此，举例来说，以下定义是合法的： even : Nat -> B